% Mizar problem: t173_orders_1,orders_1,1137,58 fof(t173_orders_1,conjecture,( ! [A] : ( v1_relat_1(A) => ! [B] : ~ ( r2_orders_1(A,B) & k3_relat_1(A) = B & r4_orders_1(A,B) & ! [C] : ~ r6_orders_1(A,C) ) ) ), inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,antisymmetry_r2_xboole_0,cc1_finset_1,cc1_ordinal1,cc1_relset_1,cc2_finset_1,cc2_ordinal1,cc3_ordinal1,commutativity_k2_tarski,commutativity_k2_xboole_0,commutativity_k3_xboole_0,connectedness_r1_ordinal1,d10_xboole_0,d11_orders_1,d12_relat_2,d14_relat_2,d16_relat_2,d1_orders_1,d1_tarski,d1_zfmisc_1,d2_ordinal1,d3_tarski,d4_relat_2,d4_xboole_0,d5_funct_1,d5_orders_1,d5_tarski,d6_relat_1,d6_relat_2,d6_wellord1,d7_orders_1,d7_ordinal1,d8_relat_2,d8_xboole_0,d9_orders_1,d9_relat_2,dt_k1_funct_1,dt_k1_relat_1,dt_k1_tarski,dt_k1_xboole_0,dt_k1_zfmisc_1,dt_k2_ordinal1,dt_k2_relat_1,dt_k2_tarski,dt_k2_wellord1,dt_k2_xboole_0,dt_k2_zfmisc_1,dt_k3_relat_1,dt_k3_tarski,dt_k3_xboole_0,dt_k4_tarski,dt_k4_xboole_0,dt_k7_relat_1,dt_m1_orders_1,dt_m1_ordinal1,dt_m1_relset_1,dt_m1_subset_1,dt_m2_relset_1,existence_m1_orders_1,existence_m1_ordinal1,existence_m1_relset_1,existence_m1_subset_1,existence_m2_relset_1,fc10_finset_1,fc11_finset_1,fc12_finset_1,fc14_finset_1,fc1_finset_1,fc1_subset_1,fc2_finset_1,fc2_ordinal1,fc2_subset_1,fc3_subset_1,fc4_ordinal1,fc4_subset_1,fc5_ordinal1,fc9_finset_1,fraenkel_a_3_0_orders_1,fraenkel_a_4_0_orders_1,fraenkel_a_4_1_orders_1,idempotence_k2_xboole_0,idempotence_k3_xboole_0,irreflexivity_r2_xboole_0,rc1_finset_1,rc1_ordinal1,rc1_partfun1,rc1_subset_1,rc2_ordinal1,rc2_partfun1,rc2_subset_1,rc3_finset_1,rc3_ordinal1,rc4_finset_1,rc4_ordinal1,redefinition_k2_ordinal1,redefinition_m2_relset_1,redefinition_r1_ordinal1,reflexivity_r1_ordinal1,reflexivity_r1_tarski,s1_ordinal1__e23_87__orders_1,s1_tarski__e5_87_8__orders_1,s1_xboole_0__e25_87__orders_1,s2_funct_1__e14_87__orders_1,s2_funct_1__e4_87_8_1__orders_1,s2_ordinal1__e3_87_8__orders_1,s2_ordinal1__e5_87_5__orders_1,s2_ordinal1__e8_87_6__orders_1,s4_ordinal1__e2_87_9__orders_1,spc0_boole,t106_zfmisc_1,t149_orders_1,t16_wellord1,t19_ordinal1,t19_wellord1,t1_boole,t1_subset,t1_xboole_1,t21_ordinal1,t22_wellord1,t23_ordinal1,t24_ordinal1,t24_wellord1,t25_wellord1,t2_boole,t2_subset,t2_tarski,t2_xboole_1,t38_ordinal1,t3_boole,t3_subset,t4_boole,t4_subset,t5_subset,t65_relat_1,t6_boole,t70_funct_1,t72_funct_1,t7_boole,t7_ordinal1,t82_funct_1,t8_boole,t91_relat_1,t97_relat_1,t9_funct_1]), [file(orders_1,t173_orders_1)]). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(antisymmetry_r2_xboole_0,axiom,( ! [A,B] : ( r2_xboole_0(A,B) => ~ r2_xboole_0(B,A) ) ), file(xboole_0,r2_xboole_0), []). fof(cc1_finset_1,axiom,( ! [A] : ( v1_xboole_0(A) => v1_finset_1(A) ) ), file(finset_1,cc1_finset_1), []). fof(cc1_ordinal1,axiom,( ! [A] : ( v3_ordinal1(A) => ( v1_ordinal1(A) & v2_ordinal1(A) ) ) ), file(ordinal1,cc1_ordinal1), []). fof(cc1_relset_1,axiom,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) => v1_relat_1(C) ) ), file(relset_1,cc1_relset_1), []). fof(cc2_finset_1,axiom,( ! [A] : ( v1_finset_1(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => v1_finset_1(B) ) ) ), file(finset_1,cc2_finset_1), []). fof(cc2_ordinal1,axiom,( ! [A] : ( ( v1_ordinal1(A) & v2_ordinal1(A) ) => v3_ordinal1(A) ) ), file(ordinal1,cc2_ordinal1), []). fof(cc3_ordinal1,axiom,( ! [A] : ( v1_xboole_0(A) => ( v1_ordinal1(A) & v2_ordinal1(A) & v3_ordinal1(A) ) ) ), file(ordinal1,cc3_ordinal1), []). fof(commutativity_k2_tarski,axiom,( ! [A,B] : k2_tarski(A,B) = k2_tarski(B,A) ), file(tarski,k2_tarski), []). fof(commutativity_k2_xboole_0,axiom,( ! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A) ), file(xboole_0,k2_xboole_0), []). fof(commutativity_k3_xboole_0,axiom,( ! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) ), file(xboole_0,k3_xboole_0), []). fof(connectedness_r1_ordinal1,axiom,( ! [A,B] : ( ( v3_ordinal1(A) & v3_ordinal1(B) ) => ( r1_ordinal1(A,B) | r1_ordinal1(B,A) ) ) ), file(ordinal1,r1_ordinal1), []). fof(d10_xboole_0,axiom,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), []). fof(d11_orders_1,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r6_orders_1(A,B) <=> ( r2_hidden(B,k3_relat_1(A)) & ! [C] : ~ ( r2_hidden(C,k3_relat_1(A)) & C != B & r2_hidden(k4_tarski(B,C),A) ) ) ) ) ), file(orders_1,d11_orders_1), []). fof(d12_relat_2,axiom,( ! [A] : ( v1_relat_1(A) => ( v4_relat_2(A) <=> r4_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d12_relat_2), []). fof(d14_relat_2,axiom,( ! [A] : ( v1_relat_1(A) => ( v6_relat_2(A) <=> r6_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d14_relat_2), []). fof(d16_relat_2,axiom,( ! [A] : ( v1_relat_1(A) => ( v8_relat_2(A) <=> r8_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d16_relat_2), []). fof(d1_orders_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ( ~ r2_hidden(k1_xboole_0,A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,A,k3_tarski(A)) & m2_relset_1(B,A,k3_tarski(A)) ) => ( m1_orders_1(B,A) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(k1_funct_1(B,C),C) ) ) ) ) ) ), file(orders_1,d1_orders_1), []). fof(d1_tarski,axiom,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), []). fof(d1_zfmisc_1,axiom,( ! [A,B] : ( B = k1_zfmisc_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> r1_tarski(C,A) ) ) ), file(zfmisc_1,d1_zfmisc_1), []). fof(d2_ordinal1,axiom,( ! [A] : ( v1_ordinal1(A) <=> ! [B] : ( r2_hidden(B,A) => r1_tarski(B,A) ) ) ), file(ordinal1,d2_ordinal1), []). fof(d3_tarski,axiom,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), []). fof(d4_relat_2,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r4_relat_2(A,B) <=> ! [C,D] : ( ( r2_hidden(C,B) & r2_hidden(D,B) & r2_hidden(k4_tarski(C,D),A) & r2_hidden(k4_tarski(D,C),A) ) => C = D ) ) ) ), file(relat_2,d4_relat_2), []). fof(d4_xboole_0,axiom,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), []). fof(d5_funct_1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), []). fof(d5_orders_1,axiom,( ! [A] : ( v1_relat_1(A) => ( v3_orders_1(A) <=> ( v1_relat_2(A) & v8_relat_2(A) & v4_relat_2(A) & v6_relat_2(A) ) ) ) ), file(orders_1,d5_orders_1), []). fof(d5_tarski,axiom,( ! [A,B] : k4_tarski(A,B) = k2_tarski(k2_tarski(A,B),k1_tarski(A)) ), file(tarski,d5_tarski), []). fof(d6_relat_1,axiom,( ! [A] : ( v1_relat_1(A) => k3_relat_1(A) = k2_xboole_0(k1_relat_1(A),k2_relat_1(A)) ) ), file(relat_1,d6_relat_1), []). fof(d6_relat_2,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r6_relat_2(A,B) <=> ! [C,D] : ~ ( r2_hidden(C,B) & r2_hidden(D,B) & C != D & ~ r2_hidden(k4_tarski(C,D),A) & ~ r2_hidden(k4_tarski(D,C),A) ) ) ) ), file(relat_2,d6_relat_2), []). fof(d6_wellord1,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : k2_wellord1(A,B) = k3_xboole_0(A,k2_zfmisc_1(B,B)) ) ), file(wellord1,d6_wellord1), []). fof(d7_orders_1,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r2_orders_1(A,B) <=> ( r1_relat_2(A,B) & r8_relat_2(A,B) & r4_relat_2(A,B) ) ) ) ), file(orders_1,d7_orders_1), []). fof(d7_ordinal1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v5_ordinal1(A) <=> v3_ordinal1(k1_relat_1(A)) ) ) ), file(ordinal1,d7_ordinal1), []). fof(d8_relat_2,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r8_relat_2(A,B) <=> ! [C,D,E] : ( ( r2_hidden(C,B) & r2_hidden(D,B) & r2_hidden(E,B) & r2_hidden(k4_tarski(C,D),A) & r2_hidden(k4_tarski(D,E),A) ) => r2_hidden(k4_tarski(C,E),A) ) ) ) ), file(relat_2,d8_relat_2), []). fof(d8_xboole_0,axiom,( ! [A,B] : ( r2_xboole_0(A,B) <=> ( r1_tarski(A,B) & A != B ) ) ), file(xboole_0,d8_xboole_0), []). fof(d9_orders_1,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : ( r4_orders_1(A,B) <=> ! [C] : ~ ( r1_tarski(C,B) & v3_orders_1(k2_wellord1(A,C)) & ! [D] : ~ ( r2_hidden(D,B) & ! [E] : ( r2_hidden(E,C) => r2_hidden(k4_tarski(E,D),A) ) ) ) ) ) ), file(orders_1,d9_orders_1), []). fof(d9_relat_2,axiom,( ! [A] : ( v1_relat_1(A) => ( v1_relat_2(A) <=> r1_relat_2(A,k3_relat_1(A)) ) ) ), file(relat_2,d9_relat_2), []). fof(dt_k1_funct_1,axiom,( $true ), file(funct_1,k1_funct_1), []). fof(dt_k1_relat_1,axiom,( $true ), file(relat_1,k1_relat_1), []). fof(dt_k1_tarski,axiom,( $true ), file(tarski,k1_tarski), []). fof(dt_k1_xboole_0,axiom,( $true ), file(xboole_0,k1_xboole_0), []). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), []). fof(dt_k2_ordinal1,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_funct_1(A) & v5_ordinal1(A) & v3_ordinal1(B) ) => m1_ordinal1(k2_ordinal1(A,B),k2_relat_1(A)) ) ), file(ordinal1,k2_ordinal1), []). fof(dt_k2_relat_1,axiom,( $true ), file(relat_1,k2_relat_1), []). fof(dt_k2_tarski,axiom,( $true ), file(tarski,k2_tarski), []). fof(dt_k2_wellord1,axiom,( ! [A,B] : ( v1_relat_1(A) => v1_relat_1(k2_wellord1(A,B)) ) ), file(wellord1,k2_wellord1), []). fof(dt_k2_xboole_0,axiom,( $true ), file(xboole_0,k2_xboole_0), []). fof(dt_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), []). fof(dt_k3_relat_1,axiom,( $true ), file(relat_1,k3_relat_1), []). fof(dt_k3_tarski,axiom,( $true ), file(tarski,k3_tarski), []). fof(dt_k3_xboole_0,axiom,( $true ), file(xboole_0,k3_xboole_0), []). fof(dt_k4_tarski,axiom,( $true ), file(tarski,k4_tarski), []). fof(dt_k4_xboole_0,axiom,( $true ), file(xboole_0,k4_xboole_0), []). fof(dt_k7_relat_1,axiom,( ! [A,B] : ( v1_relat_1(A) => v1_relat_1(k7_relat_1(A,B)) ) ), file(relat_1,k7_relat_1), []). fof(dt_m1_orders_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_orders_1(B,A) => ( v1_funct_1(B) & v1_funct_2(B,A,k3_tarski(A)) & m2_relset_1(B,A,k3_tarski(A)) ) ) ) ), file(orders_1,m1_orders_1), []). fof(dt_m1_ordinal1,axiom,( ! [A,B] : ( m1_ordinal1(B,A) => ( v1_relat_1(B) & v1_funct_1(B) & v5_ordinal1(B) ) ) ), file(ordinal1,m1_ordinal1), []). fof(dt_m1_relset_1,axiom,( $true ), file(relset_1,m1_relset_1), []). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), []). fof(dt_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ), file(relset_1,m2_relset_1), []). fof(existence_m1_orders_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : m1_orders_1(B,A) ) ), file(orders_1,m1_orders_1), []). fof(existence_m1_ordinal1,axiom,( ! [A] : ? [B] : m1_ordinal1(B,A) ), file(ordinal1,m1_ordinal1), []). fof(existence_m1_relset_1,axiom,( ! [A,B] : ? [C] : m1_relset_1(C,A,B) ), file(relset_1,m1_relset_1), []). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), []). fof(existence_m2_relset_1,axiom,( ! [A,B] : ? [C] : m2_relset_1(C,A,B) ), file(relset_1,m2_relset_1), []). fof(fc10_finset_1,axiom,( ! [A,B] : ( v1_finset_1(B) => v1_finset_1(k3_xboole_0(A,B)) ) ), file(finset_1,fc10_finset_1), []). fof(fc11_finset_1,axiom,( ! [A,B] : ( v1_finset_1(A) => v1_finset_1(k3_xboole_0(A,B)) ) ), file(finset_1,fc11_finset_1), []). fof(fc12_finset_1,axiom,( ! [A,B] : ( v1_finset_1(A) => v1_finset_1(k4_xboole_0(A,B)) ) ), file(finset_1,fc12_finset_1), []). fof(fc14_finset_1,axiom,( ! [A,B] : ( ( v1_finset_1(A) & v1_finset_1(B) ) => v1_finset_1(k2_zfmisc_1(A,B)) ) ), file(finset_1,fc14_finset_1), []). fof(fc1_finset_1,axiom,( ! [A] : ( ~ v1_xboole_0(k1_tarski(A)) & v1_finset_1(k1_tarski(A)) ) ), file(finset_1,fc1_finset_1), []). fof(fc1_subset_1,axiom,( ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ), file(subset_1,fc1_subset_1), []). fof(fc2_finset_1,axiom,( ! [A,B] : ( ~ v1_xboole_0(k2_tarski(A,B)) & v1_finset_1(k2_tarski(A,B)) ) ), file(finset_1,fc2_finset_1), []). fof(fc2_ordinal1,axiom, ( v1_relat_1(k1_xboole_0) & v3_relat_1(k1_xboole_0) & v1_funct_1(k1_xboole_0) & v2_funct_1(k1_xboole_0) & v1_xboole_0(k1_xboole_0) & v1_ordinal1(k1_xboole_0) & v2_ordinal1(k1_xboole_0) & v3_ordinal1(k1_xboole_0) ), file(ordinal1,fc2_ordinal1), []). fof(fc2_subset_1,axiom,( ! [A] : ~ v1_xboole_0(k1_tarski(A)) ), file(subset_1,fc2_subset_1), []). fof(fc3_subset_1,axiom,( ! [A,B] : ~ v1_xboole_0(k2_tarski(A,B)) ), file(subset_1,fc3_subset_1), []). fof(fc4_ordinal1,axiom,( ! [A] : ( v3_ordinal1(A) => ( v1_ordinal1(k3_tarski(A)) & v2_ordinal1(k3_tarski(A)) & v3_ordinal1(k3_tarski(A)) ) ) ), file(ordinal1,fc4_ordinal1), []). fof(fc4_subset_1,axiom,( ! [A,B] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) ) => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ), file(subset_1,fc4_subset_1), []). fof(fc5_ordinal1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v5_ordinal1(A) ) => ( v1_ordinal1(k1_relat_1(A)) & v2_ordinal1(k1_relat_1(A)) & v3_ordinal1(k1_relat_1(A)) ) ) ), file(ordinal1,fc5_ordinal1), []). fof(fc9_finset_1,axiom,( ! [A,B] : ( ( v1_finset_1(A) & v1_finset_1(B) ) => v1_finset_1(k2_xboole_0(A,B)) ) ), file(finset_1,fc9_finset_1), []). fof(fraenkel_a_3_0_orders_1,axiom,( ! [A,B,C,D] : ( ( v1_relat_1(B) & ~ v1_xboole_0(C) & v1_relat_1(D) & v1_funct_1(D) & v5_ordinal1(D) ) => ( r2_hidden(A,a_3_0_orders_1(B,C,D)) <=> ? [E] : ( m1_subset_1(E,C) & A = E & ! [F] : ( r2_hidden(F,k2_relat_1(D)) => ( F != E & r2_hidden(k4_tarski(F,E),B) ) ) ) ) ) ), file(orders_1,a_3_0_orders_1), []). fof(fraenkel_a_4_0_orders_1,axiom,( ! [A,B,C,D,E] : ( ( v1_relat_1(B) & ~ v1_xboole_0(C) & v1_relat_1(D) & v1_funct_1(D) & v5_ordinal1(D) & v3_ordinal1(E) ) => ( r2_hidden(A,a_4_0_orders_1(B,C,D,E)) <=> ? [F] : ( m1_subset_1(F,C) & A = F & ! [G] : ( r2_hidden(G,k2_relat_1(k2_ordinal1(D,E))) => ( G != F & r2_hidden(k4_tarski(G,F),B) ) ) ) ) ) ), file(orders_1,a_4_0_orders_1), []). fof(fraenkel_a_4_1_orders_1,axiom,( ! [A,B,C,D,E] : ( ( v1_relat_1(B) & ~ v1_xboole_0(C) & v3_ordinal1(D) & v1_relat_1(E) & v1_funct_1(E) & v5_ordinal1(E) ) => ( r2_hidden(A,a_4_1_orders_1(B,C,D,E)) <=> ? [F] : ( m1_subset_1(F,C) & A = F & ! [G] : ( r2_hidden(G,k2_relat_1(k2_ordinal1(E,D))) => ( G != F & r2_hidden(k4_tarski(G,F),B) ) ) ) ) ) ), file(orders_1,a_4_1_orders_1), []). fof(idempotence_k2_xboole_0,axiom,( ! [A,B] : k2_xboole_0(A,A) = A ), file(xboole_0,k2_xboole_0), []). fof(idempotence_k3_xboole_0,axiom,( ! [A,B] : k3_xboole_0(A,A) = A ), file(xboole_0,k3_xboole_0), []). fof(irreflexivity_r2_xboole_0,axiom,( ! [A,B] : ~ r2_xboole_0(A,A) ), file(xboole_0,r2_xboole_0), []). fof(rc1_finset_1,axiom,( ? [A] : ( ~ v1_xboole_0(A) & v1_finset_1(A) ) ), file(finset_1,rc1_finset_1), []). fof(rc1_ordinal1,axiom,( ? [A] : ( v1_ordinal1(A) & v2_ordinal1(A) & v3_ordinal1(A) ) ), file(ordinal1,rc1_ordinal1), []). fof(rc1_partfun1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) & v1_xboole_0(A) ) ), file(partfun1,rc1_partfun1), []). fof(rc1_subset_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_xboole_0(B) ) ) ), file(subset_1,rc1_subset_1), []). fof(rc2_ordinal1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) & v1_xboole_0(A) & v1_ordinal1(A) & v2_ordinal1(A) & v3_ordinal1(A) ) ), file(ordinal1,rc2_ordinal1), []). fof(rc2_partfun1,axiom,( ! [A,B] : ? [C] : ( m1_relset_1(C,A,B) & v1_relat_1(C) & v1_funct_1(C) ) ), file(partfun1,rc2_partfun1), []). fof(rc2_subset_1,axiom,( ! [A] : ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & v1_xboole_0(B) ) ), file(subset_1,rc2_subset_1), []). fof(rc3_finset_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_xboole_0(B) & v1_finset_1(B) ) ) ), file(finset_1,rc3_finset_1), []). fof(rc3_ordinal1,axiom,( ? [A] : ( ~ v1_xboole_0(A) & v1_ordinal1(A) & v2_ordinal1(A) & v3_ordinal1(A) ) ), file(ordinal1,rc3_ordinal1), []). fof(rc4_finset_1,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_xboole_0(B) & v1_finset_1(B) ) ) ), file(finset_1,rc4_finset_1), []). fof(rc4_ordinal1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v5_ordinal1(A) ) ), file(ordinal1,rc4_ordinal1), []). fof(redefinition_k2_ordinal1,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_funct_1(A) & v5_ordinal1(A) & v3_ordinal1(B) ) => k2_ordinal1(A,B) = k7_relat_1(A,B) ) ), file(ordinal1,k2_ordinal1), []). fof(redefinition_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) <=> m1_relset_1(C,A,B) ) ), file(relset_1,m2_relset_1), []). fof(redefinition_r1_ordinal1,axiom,( ! [A,B] : ( ( v3_ordinal1(A) & v3_ordinal1(B) ) => ( r1_ordinal1(A,B) <=> r1_tarski(A,B) ) ) ), file(ordinal1,r1_ordinal1), []). fof(reflexivity_r1_ordinal1,axiom,( ! [A,B] : ( ( v3_ordinal1(A) & v3_ordinal1(B) ) => r1_ordinal1(A,A) ) ), file(ordinal1,r1_ordinal1), []). fof(reflexivity_r1_tarski,axiom,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), []). fof(s1_ordinal1__e23_87__orders_1,axiom,( ! [A,B,C] : ( ( v1_relat_1(A) & ~ v1_xboole_0(B) & v1_relat_1(C) & v1_funct_1(C) ) => ( ? [D] : ( v3_ordinal1(D) & ? [E] : ( v1_relat_1(E) & v1_funct_1(E) & v5_ordinal1(E) & B = k1_funct_1(C,a_3_0_orders_1(A,B,E)) & k1_relat_1(E) = D & ! [F] : ( v3_ordinal1(F) => ! [G] : ( ( v1_relat_1(G) & v1_funct_1(G) & v5_ordinal1(G) ) => ( ( r2_hidden(F,D) & G = k2_ordinal1(E,F) ) => k1_funct_1(E,F) = k1_funct_1(C,a_3_0_orders_1(A,B,G)) ) ) ) ) ) => ? [D] : ( v3_ordinal1(D) & ? [H] : ( v1_relat_1(H) & v1_funct_1(H) & v5_ordinal1(H) & B = k1_funct_1(C,a_3_0_orders_1(A,B,H)) & k1_relat_1(H) = D & ! [I] : ( v3_ordinal1(I) => ! [J] : ( ( v1_relat_1(J) & v1_funct_1(J) & v5_ordinal1(J) ) => ( ( r2_hidden(I,D) & J = k2_ordinal1(H,I) ) => k1_funct_1(H,I) = k1_funct_1(C,a_3_0_orders_1(A,B,J)) ) ) ) ) & ! [K] : ( v3_ordinal1(K) => ( ? [L] : ( v1_relat_1(L) & v1_funct_1(L) & v5_ordinal1(L) & B = k1_funct_1(C,a_3_0_orders_1(A,B,L)) & k1_relat_1(L) = K & ! [M] : ( v3_ordinal1(M) => ! [N] : ( ( v1_relat_1(N) & v1_funct_1(N) & v5_ordinal1(N) ) => ( ( r2_hidden(M,K) & N = k2_ordinal1(L,M) ) => k1_funct_1(L,M) = k1_funct_1(C,a_3_0_orders_1(A,B,N)) ) ) ) ) => r1_ordinal1(D,K) ) ) ) ) ) ), file(orders_1,s1_ordinal1__e23_87__orders_1), []). fof(s1_tarski__e5_87_8__orders_1,axiom,( ! [A,B,C] : ( ( v1_relat_1(A) & ~ v1_xboole_0(B) & v1_relat_1(C) & v1_funct_1(C) ) => ( ! [D,E,F] : ( ( ? [G] : ( v3_ordinal1(G) & E = G & ? [H] : ( v1_relat_1(H) & v1_funct_1(H) & v5_ordinal1(H) & D = k1_funct_1(C,a_3_0_orders_1(A,B,H)) & k1_relat_1(H) = G & ! [I] : ( v3_ordinal1(I) => ! [J] : ( ( v1_relat_1(J) & v1_funct_1(J) & v5_ordinal1(J) ) => ( ( r2_hidden(I,G) & J = k2_ordinal1(H,I) ) => k1_funct_1(H,I) = k1_funct_1(C,a_3_0_orders_1(A,B,J)) ) ) ) ) ) & ? [K] : ( v3_ordinal1(K) & F = K & ? [L] : ( v1_relat_1(L) & v1_funct_1(L) & v5_ordinal1(L) & D = k1_funct_1(C,a_3_0_orders_1(A,B,L)) & k1_relat_1(L) = K & ! [M] : ( v3_ordinal1(M) => ! [N] : ( ( v1_relat_1(N) & v1_funct_1(N) & v5_ordinal1(N) ) => ( ( r2_hidden(M,K) & N = k2_ordinal1(L,M) ) => k1_funct_1(L,M) = k1_funct_1(C,a_3_0_orders_1(A,B,N)) ) ) ) ) ) ) => E = F ) => ? [D] : ! [E] : ( r2_hidden(E,D) <=> ? [F] : ( r2_hidden(F,B) & ? [O] : ( v3_ordinal1(O) & E = O & ? [P] : ( v1_relat_1(P) & v1_funct_1(P) & v5_ordinal1(P) & F = k1_funct_1(C,a_3_0_orders_1(A,B,P)) & k1_relat_1(P) = O & ! [Q] : ( v3_ordinal1(Q) => ! [R] : ( ( v1_relat_1(R) & v1_funct_1(R) & v5_ordinal1(R) ) => ( ( r2_hidden(Q,O) & R = k2_ordinal1(P,Q) ) => k1_funct_1(P,Q) = k1_funct_1(C,a_3_0_orders_1(A,B,R)) ) ) ) ) ) ) ) ) ) ), file(orders_1,s1_tarski__e5_87_8__orders_1), []). fof(s1_xboole_0__e25_87__orders_1,axiom,( ! [A,B,C,D] : ( ( v1_relat_1(A) & ~ v1_xboole_0(B) & v1_relat_1(C) & v1_funct_1(C) & v3_ordinal1(D) ) => ? [E] : ! [F] : ( r2_hidden(F,E) <=> ( r2_hidden(F,B) & ? [G] : ( v3_ordinal1(G) & r2_hidden(G,D) & ? [H] : ( v1_relat_1(H) & v1_funct_1(H) & v5_ordinal1(H) & F = k1_funct_1(C,a_3_0_orders_1(A,B,H)) & k1_relat_1(H) = G & ! [I] : ( v3_ordinal1(I) => ! [J] : ( ( v1_relat_1(J) & v1_funct_1(J) & v5_ordinal1(J) ) => ( ( r2_hidden(I,G) & J = k2_ordinal1(H,I) ) => k1_funct_1(H,I) = k1_funct_1(C,a_3_0_orders_1(A,B,J)) ) ) ) ) ) ) ) ) ), file(orders_1,s1_xboole_0__e25_87__orders_1), []). fof(s2_funct_1__e14_87__orders_1,axiom,( ! [A,B,C] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & m1_orders_1(C,B) ) => ( ( ! [D,E,F] : ( ( r2_hidden(D,k1_zfmisc_1(A)) & ( ( D != k1_xboole_0 & E = k1_funct_1(C,D) ) | ( D = k1_xboole_0 & E = A ) ) & ( ( D != k1_xboole_0 & F = k1_funct_1(C,D) ) | ( D = k1_xboole_0 & F = A ) ) ) => E = F ) & ! [D] : ~ ( r2_hidden(D,k1_zfmisc_1(A)) & ! [E] : ~ ( ( D != k1_xboole_0 & E = k1_funct_1(C,D) ) | ( D = k1_xboole_0 & E = A ) ) ) ) => ? [D] : ( v1_relat_1(D) & v1_funct_1(D) & k1_relat_1(D) = k1_zfmisc_1(A) & ! [E] : ( r2_hidden(E,k1_zfmisc_1(A)) => ( ( E != k1_xboole_0 & k1_funct_1(D,E) = k1_funct_1(C,E) ) | ( E = k1_xboole_0 & k1_funct_1(D,E) = A ) ) ) ) ) ) ), file(orders_1,s2_funct_1__e14_87__orders_1), []). fof(s2_funct_1__e4_87_8_1__orders_1,axiom,( ! [A,B,C,D] : ( ( v1_relat_1(A) & ~ v1_xboole_0(B) & v1_relat_1(C) & v1_funct_1(C) & v3_ordinal1(D) ) => ( ( ! [E,F,G] : ( ( r2_hidden(E,D) & ? [H] : ( v3_ordinal1(H) & E = H & ? [I] : ( v1_relat_1(I) & v1_funct_1(I) & v5_ordinal1(I) & F = k1_funct_1(C,a_3_0_orders_1(A,B,I)) & k1_relat_1(I) = H & ! [J] : ( v3_ordinal1(J) => ! [K] : ( ( v1_relat_1(K) & v1_funct_1(K) & v5_ordinal1(K) ) => ( ( r2_hidden(J,H) & K = k2_ordinal1(I,J) ) => k1_funct_1(I,J) = k1_funct_1(C,a_3_0_orders_1(A,B,K)) ) ) ) ) ) & ? [L] : ( v3_ordinal1(L) & E = L & ? [M] : ( v1_relat_1(M) & v1_funct_1(M) & v5_ordinal1(M) & G = k1_funct_1(C,a_3_0_orders_1(A,B,M)) & k1_relat_1(M) = L & ! [N] : ( v3_ordinal1(N) => ! [O] : ( ( v1_relat_1(O) & v1_funct_1(O) & v5_ordinal1(O) ) => ( ( r2_hidden(N,L) & O = k2_ordinal1(M,N) ) => k1_funct_1(M,N) = k1_funct_1(C,a_3_0_orders_1(A,B,O)) ) ) ) ) ) ) => F = G ) & ! [E] : ~ ( r2_hidden(E,D) & ! [F] : ~ ? [P] : ( v3_ordinal1(P) & E = P & ? [Q] : ( v1_relat_1(Q) & v1_funct_1(Q) & v5_ordinal1(Q) & F = k1_funct_1(C,a_3_0_orders_1(A,B,Q)) & k1_relat_1(Q) = P & ! [R] : ( v3_ordinal1(R) => ! [S] : ( ( v1_relat_1(S) & v1_funct_1(S) & v5_ordinal1(S) ) => ( ( r2_hidden(R,P) & S = k2_ordinal1(Q,R) ) => k1_funct_1(Q,R) = k1_funct_1(C,a_3_0_orders_1(A,B,S)) ) ) ) ) ) ) ) => ? [E] : ( v1_relat_1(E) & v1_funct_1(E) & k1_relat_1(E) = D & ! [F] : ( r2_hidden(F,D) => ? [T] : ( v3_ordinal1(T) & F = T & ? [U] : ( v1_relat_1(U) & v1_funct_1(U) & v5_ordinal1(U) & k1_funct_1(E,F) = k1_funct_1(C,a_3_0_orders_1(A,B,U)) & k1_relat_1(U) = T & ! [V] : ( v3_ordinal1(V) => ! [W] : ( ( v1_relat_1(W) & v1_funct_1(W) & v5_ordinal1(W) ) => ( ( r2_hidden(V,T) & W = k2_ordinal1(U,V) ) => k1_funct_1(U,V) = k1_funct_1(C,a_3_0_orders_1(A,B,W)) ) ) ) ) ) ) ) ) ) ), file(orders_1,s2_funct_1__e4_87_8_1__orders_1), []). fof(s2_ordinal1__e3_87_8__orders_1,axiom,( ! [A,B,C] : ( ( v1_relat_1(A) & ~ v1_xboole_0(B) & v1_relat_1(C) & v1_funct_1(C) ) => ( ! [D] : ( v3_ordinal1(D) => ( ! [E] : ( v3_ordinal1(E) => ( r2_hidden(E,D) => ? [F] : ( m1_subset_1(F,B) & ? [G] : ( v1_relat_1(G) & v1_funct_1(G) & v5_ordinal1(G) & F = k1_funct_1(C,a_3_0_orders_1(A,B,G)) & k1_relat_1(G) = E & ! [H] : ( v3_ordinal1(H) => ! [I] : ( ( v1_relat_1(I) & v1_funct_1(I) & v5_ordinal1(I) ) => ( ( r2_hidden(H,E) & I = k2_ordinal1(G,H) ) => k1_funct_1(G,H) = k1_funct_1(C,a_3_0_orders_1(A,B,I)) ) ) ) ) ) ) ) => ? [J] : ( m1_subset_1(J,B) & ? [K] : ( v1_relat_1(K) & v1_funct_1(K) & v5_ordinal1(K) & J = k1_funct_1(C,a_3_0_orders_1(A,B,K)) & k1_relat_1(K) = D & ! [L] : ( v3_ordinal1(L) => ! [M] : ( ( v1_relat_1(M) & v1_funct_1(M) & v5_ordinal1(M) ) => ( ( r2_hidden(L,D) & M = k2_ordinal1(K,L) ) => k1_funct_1(K,L) = k1_funct_1(C,a_3_0_orders_1(A,B,M)) ) ) ) ) ) ) ) => ! [D] : ( v3_ordinal1(D) => ? [N] : ( m1_subset_1(N,B) & ? [O] : ( v1_relat_1(O) & v1_funct_1(O) & v5_ordinal1(O) & N = k1_funct_1(C,a_3_0_orders_1(A,B,O)) & k1_relat_1(O) = D & ! [P] : ( v3_ordinal1(P) => ! [Q] : ( ( v1_relat_1(Q) & v1_funct_1(Q) & v5_ordinal1(Q) ) => ( ( r2_hidden(P,D) & Q = k2_ordinal1(O,P) ) => k1_funct_1(O,P) = k1_funct_1(C,a_3_0_orders_1(A,B,Q)) ) ) ) ) ) ) ) ) ), file(orders_1,s2_ordinal1__e3_87_8__orders_1), []). fof(s2_ordinal1__e5_87_5__orders_1,axiom,( ! [A,B,C] : ( ( v1_relat_1(A) & v1_funct_1(A) & v5_ordinal1(A) & v1_relat_1(B) & v1_funct_1(B) & v5_ordinal1(B) & v3_ordinal1(C) ) => ( ! [D] : ( v3_ordinal1(D) => ( ! [E] : ( v3_ordinal1(E) => ( r2_hidden(E,D) => ( r1_ordinal1(E,C) => k2_ordinal1(A,E) = k2_ordinal1(B,E) ) ) ) => ( r1_ordinal1(D,C) => k2_ordinal1(A,D) = k2_ordinal1(B,D) ) ) ) => ! [D] : ( v3_ordinal1(D) => ( r1_ordinal1(D,C) => k2_ordinal1(A,D) = k2_ordinal1(B,D) ) ) ) ) ), file(orders_1,s2_ordinal1__e5_87_5__orders_1), []). fof(s2_ordinal1__e8_87_6__orders_1,axiom,( ! [A,B,C] : ( ( v3_ordinal1(A) & v1_relat_1(B) & v1_funct_1(B) & v5_ordinal1(B) & v1_relat_1(C) & v1_funct_1(C) & v5_ordinal1(C) ) => ( ! [D] : ( v3_ordinal1(D) => ( ! [E] : ( v3_ordinal1(E) => ( r2_hidden(E,D) => ( r1_ordinal1(E,A) => k2_ordinal1(B,E) = k2_ordinal1(C,E) ) ) ) => ( r1_ordinal1(D,A) => k2_ordinal1(B,D) = k2_ordinal1(C,D) ) ) ) => ! [D] : ( v3_ordinal1(D) => ( r1_ordinal1(D,A) => k2_ordinal1(B,D) = k2_ordinal1(C,D) ) ) ) ) ), file(orders_1,s2_ordinal1__e8_87_6__orders_1), []). fof(s4_ordinal1__e2_87_9__orders_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v5_ordinal1(A) & k1_relat_1(A) = k1_xboole_0 & ! [B] : ( v3_ordinal1(B) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v5_ordinal1(C) ) => ( ( r2_hidden(B,k1_xboole_0) & C = k2_ordinal1(A,B) ) => k1_funct_1(A,B) = 0 ) ) ) ) ), file(orders_1,s4_ordinal1__e2_87_9__orders_1), []). fof(spc0_boole,axiom,( v1_xboole_0(0) ), file(boole,spc0_boole), []). fof(t106_zfmisc_1,axiom,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), []). fof(t149_orders_1,axiom,( ! [A] : ( v1_relat_1(A) => ! [B] : ~ ( r4_orders_1(A,B) & B = k1_xboole_0 ) ) ), file(orders_1,t149_orders_1), []). fof(t16_wellord1,axiom,( ! [A,B,C] : ( v1_relat_1(C) => ( r2_hidden(A,k2_wellord1(C,B)) <=> ( r2_hidden(A,C) & r2_hidden(A,k2_zfmisc_1(B,B)) ) ) ) ), file(wellord1,t16_wellord1), []). fof(t19_ordinal1,axiom,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ! [C] : ( v1_ordinal1(C) => ( ( r2_hidden(C,A) & r2_hidden(A,B) ) => r2_hidden(C,B) ) ) ) ) ), file(ordinal1,t19_ordinal1), []). fof(t19_wellord1,axiom,( ! [A,B,C] : ( v1_relat_1(C) => ( r2_hidden(A,k3_relat_1(k2_wellord1(C,B))) => ( r2_hidden(A,k3_relat_1(C)) & r2_hidden(A,B) ) ) ) ), file(wellord1,t19_wellord1), []). fof(t1_boole,axiom,( ! [A] : k2_xboole_0(A,k1_xboole_0) = A ), file(boole,t1_boole), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t1_xboole_1,axiom,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), []). fof(t21_ordinal1,axiom,( ! [A] : ( v1_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ( r2_xboole_0(A,B) => r2_hidden(A,B) ) ) ) ), file(ordinal1,t21_ordinal1), []). fof(t22_wellord1,axiom,( ! [A,B] : ( v1_relat_1(B) => ( v1_relat_2(B) => v1_relat_2(k2_wellord1(B,A)) ) ) ), file(wellord1,t22_wellord1), []). fof(t23_ordinal1,axiom,( ! [A,B] : ( v3_ordinal1(B) => ( r2_hidden(A,B) => v3_ordinal1(A) ) ) ), file(ordinal1,t23_ordinal1), []). fof(t24_ordinal1,axiom,( ! [A] : ( v3_ordinal1(A) => ! [B] : ( v3_ordinal1(B) => ~ ( ~ r2_hidden(A,B) & A != B & ~ r2_hidden(B,A) ) ) ) ), file(ordinal1,t24_ordinal1), []). fof(t24_wellord1,axiom,( ! [A,B] : ( v1_relat_1(B) => ( v8_relat_2(B) => v8_relat_2(k2_wellord1(B,A)) ) ) ), file(wellord1,t24_wellord1), []). fof(t25_wellord1,axiom,( ! [A,B] : ( v1_relat_1(B) => ( v4_relat_2(B) => v4_relat_2(k2_wellord1(B,A)) ) ) ), file(wellord1,t25_wellord1), []). fof(t2_boole,axiom,( ! [A] : k3_xboole_0(A,k1_xboole_0) = k1_xboole_0 ), file(boole,t2_boole), []). fof(t2_subset,axiom,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), []). fof(t2_tarski,axiom,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), []). fof(t2_xboole_1,axiom,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), []). fof(t38_ordinal1,axiom,( ! [A] : ~ ! [B] : ( v3_ordinal1(B) => r2_hidden(B,A) ) ), file(ordinal1,t38_ordinal1), []). fof(t3_boole,axiom,( ! [A] : k4_xboole_0(A,k1_xboole_0) = A ), file(boole,t3_boole), []). fof(t3_subset,axiom,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), []). fof(t4_boole,axiom,( ! [A] : k4_xboole_0(k1_xboole_0,A) = k1_xboole_0 ), file(boole,t4_boole), []). fof(t4_subset,axiom,( ! [A,B,C] : ( ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) ) => m1_subset_1(A,C) ) ), file(subset,t4_subset), []). fof(t5_subset,axiom,( ! [A,B,C] : ~ ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) & v1_xboole_0(C) ) ), file(subset,t5_subset), []). fof(t65_relat_1,axiom,( ! [A] : ( v1_relat_1(A) => ( k1_relat_1(A) = k1_xboole_0 <=> k2_relat_1(A) = k1_xboole_0 ) ) ), file(relat_1,t65_relat_1), []). fof(t6_boole,axiom,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), []). fof(t70_funct_1,axiom,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,k1_relat_1(k7_relat_1(C,A))) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t70_funct_1), []). fof(t72_funct_1,axiom,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,A) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t72_funct_1), []). fof(t7_boole,axiom,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), []). fof(t7_ordinal1,axiom,( ! [A,B] : ~ ( r2_hidden(A,B) & r1_tarski(B,A) ) ), file(ordinal1,t7_ordinal1), []). fof(t82_funct_1,axiom,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r1_tarski(A,B) => ( k7_relat_1(k7_relat_1(C,A),B) = k7_relat_1(C,A) & k7_relat_1(k7_relat_1(C,B),A) = k7_relat_1(C,A) ) ) ) ), file(funct_1,t82_funct_1), []). fof(t8_boole,axiom,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), []). fof(t91_relat_1,axiom,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => k1_relat_1(k7_relat_1(B,A)) = A ) ) ), file(relat_1,t91_relat_1), []). fof(t97_relat_1,axiom,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(k1_relat_1(B),A) => k7_relat_1(B,A) = B ) ) ), file(relat_1,t97_relat_1), []). fof(t9_funct_1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) => A = B ) ) ) ), file(funct_1,t9_funct_1), []).