% Mizar problem: t28_projred1,projred1,684,40 fof(t28_projred1,conjecture,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u2_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u2_incsp_1(A)) => ~ ( ~ r1_incsp_1(A,B,E) & ~ r1_incsp_1(A,B,F) & ~ r1_incsp_1(A,C,F) & ~ r1_incsp_1(A,C,G) & r1_incsp_1(A,D,E) & r1_incsp_1(A,D,F) & r1_incsp_1(A,D,G) & E != G & ! [H] : ( m1_subset_1(H,u1_incsp_1(A)) => ~ ( ~ r1_incsp_1(A,H,E) & ~ r1_incsp_1(A,H,G) & k5_relat_1(k1_projred1(A,E,F,B),k1_projred1(A,F,G,C)) = k1_projred1(A,E,G,H) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,cc1_funct_1,cc1_relset_1,cc2_funct_1,d10_incproj,d10_xboole_0,d14_incproj,d1_projred1,d3_tarski,d5_incproj,d8_incproj,d9_incproj,dt_k1_funct_1,dt_k1_projred1,dt_k1_relat_1,dt_k1_xboole_0,dt_k1_zfmisc_1,dt_k2_relat_1,dt_k2_zfmisc_1,dt_k4_relset_1,dt_k5_relat_1,dt_l1_incsp_1,dt_m1_relset_1,dt_m1_subset_1,dt_m2_relset_1,dt_u1_incsp_1,dt_u2_incsp_1,existence_l1_incsp_1,existence_m1_relset_1,existence_m1_subset_1,existence_m2_relset_1,fc1_funct_1,rc1_funct_1,rc2_funct_1,rc3_funct_1,redefinition_k4_relset_1,redefinition_m2_relset_1,reflexivity_r1_tarski,s1_xboole_0__e3_28__projred1,t11_relset_1,t12_relset_1,t14_projred1,t1_subset,t21_projred1,t22_funct_1,t22_projred1,t23_projred1,t25_projred1,t26_projred1,t27_projred1,t2_subset,t34_partfun1,t3_subset,t4_subset,t5_subset,t6_boole,t7_boole,t8_boole,t8_projred1]), [file(projred1,t28_projred1)]). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(cc1_funct_1,axiom,( ! [A] : ( v1_xboole_0(A) => v1_funct_1(A) ) ), file(funct_1,cc1_funct_1), []). 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_funct_1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) => ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ) ), file(funct_1,cc2_funct_1), []). fof(d10_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ( v2_incproj(A) <=> ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ? [D] : ( m1_subset_1(D,u2_incsp_1(A)) & r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) ) ) ) ) ) ), file(incproj,d10_incproj), []). fof(d10_xboole_0,axiom,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), []). fof(d14_incproj,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ( v6_incproj(A) <=> ! [B] : ( m1_subset_1(B,u2_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ? [D] : ( m1_subset_1(D,u1_incsp_1(A)) & r1_incsp_1(A,D,B) & r1_incsp_1(A,D,C) ) ) ) ) ) ), file(incproj,d14_incproj), []). fof(d1_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u2_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ~ ( ~ r1_incsp_1(A,D,B) & ~ r1_incsp_1(A,D,C) & ~ ! [E] : ( ( v1_funct_1(E) & m2_relset_1(E,u1_incsp_1(A),u1_incsp_1(A)) ) => ( E = k1_projred1(A,B,C,D) <=> ( r1_tarski(k4_relset_1(u1_incsp_1(A),u1_incsp_1(A),E),u1_incsp_1(A)) & ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ( r2_hidden(F,k4_relset_1(u1_incsp_1(A),u1_incsp_1(A),E)) <=> r1_incsp_1(A,F,B) ) ) & ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ( ( r1_incsp_1(A,F,B) & r1_incsp_1(A,G,C) ) => ( k1_funct_1(E,F) = G <=> ? [H] : ( m1_subset_1(H,u2_incsp_1(A)) & r1_incsp_1(A,D,H) & r1_incsp_1(A,F,H) & r1_incsp_1(A,G,H) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(projred1,d1_projred1), []). fof(d3_tarski,axiom,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), []). fof(d5_incproj,axiom,( ! [A,B,C] : ( r1_incproj(A,B,C) <=> ( A != B & B != C & C != A ) ) ), file(incproj,d5_incproj), []). fof(d8_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ( r4_incproj(A,B,C,D,E) <=> ( r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) & r1_incsp_1(A,E,D) ) ) ) ) ) ) ) ), file(incproj,d8_incproj), []). fof(d9_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ( v1_incproj(A) <=> ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ~ ( r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) & r1_incsp_1(A,B,E) & r1_incsp_1(A,C,E) & B != C & D != E ) ) ) ) ) ) ) ), file(incproj,d9_incproj), []). fof(dt_k1_funct_1,axiom,( $true ), file(funct_1,k1_funct_1), []). fof(dt_k1_projred1,axiom,( ! [A,B,C,D] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) & m1_subset_1(B,u2_incsp_1(A)) & m1_subset_1(C,u2_incsp_1(A)) & m1_subset_1(D,u1_incsp_1(A)) ) => ( v1_funct_1(k1_projred1(A,B,C,D)) & m2_relset_1(k1_projred1(A,B,C,D),u1_incsp_1(A),u1_incsp_1(A)) ) ) ), file(projred1,k1_projred1), []). fof(dt_k1_relat_1,axiom,( $true ), file(relat_1,k1_relat_1), []). 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_relat_1,axiom,( $true ), file(relat_1,k2_relat_1), []). fof(dt_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), []). fof(dt_k4_relset_1,axiom,( ! [A,B,C] : ( m1_relset_1(C,A,B) => m1_subset_1(k4_relset_1(A,B,C),k1_zfmisc_1(A)) ) ), file(relset_1,k4_relset_1), []). fof(dt_k5_relat_1,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_relat_1(B) ) => v1_relat_1(k5_relat_1(A,B)) ) ), file(relat_1,k5_relat_1), []). fof(dt_l1_incsp_1,axiom,( $true ), file(incsp_1,l1_incsp_1), []). 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(dt_u1_incsp_1,axiom,( ! [A] : ( l1_incsp_1(A) => ~ v1_xboole_0(u1_incsp_1(A)) ) ), file(incsp_1,u1_incsp_1), []). fof(dt_u2_incsp_1,axiom,( ! [A] : ( l1_incsp_1(A) => ~ v1_xboole_0(u2_incsp_1(A)) ) ), file(incsp_1,u2_incsp_1), []). fof(existence_l1_incsp_1,axiom,( ? [A] : l1_incsp_1(A) ), file(incsp_1,l1_incsp_1), []). 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(fc1_funct_1,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_relat_1(B) & v1_funct_1(B) ) => ( v1_relat_1(k5_relat_1(A,B)) & v1_funct_1(k5_relat_1(A,B)) ) ) ), file(funct_1,fc1_funct_1), []). fof(rc1_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) ) ), file(funct_1,rc1_funct_1), []). fof(rc2_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) ), file(funct_1,rc2_funct_1), []). fof(rc3_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ), file(funct_1,rc3_funct_1), []). fof(redefinition_k4_relset_1,axiom,( ! [A,B,C] : ( m1_relset_1(C,A,B) => k4_relset_1(A,B,C) = k1_relat_1(C) ) ), file(relset_1,k4_relset_1), []). 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(reflexivity_r1_tarski,axiom,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), []). fof(s1_xboole_0__e3_28__projred1,axiom,( ! [A,B] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) & m1_subset_1(B,u2_incsp_1(A)) ) => ? [C] : ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,u1_incsp_1(A)) & ? [E] : ( m1_subset_1(E,u1_incsp_1(A)) & D = E & r1_incsp_1(A,E,B) ) ) ) ) ), file(projred1,s1_xboole_0__e3_28__projred1), []). fof(t11_relset_1,axiom,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) => m2_relset_1(C,A,B) ) ) ), file(relset_1,t11_relset_1), []). fof(t12_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) ) ), file(relset_1,t12_relset_1), []). fof(t14_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ! [H] : ( m1_subset_1(H,u1_incsp_1(A)) => ! [I] : ( m1_subset_1(I,u1_incsp_1(A)) => ! [J] : ( m1_subset_1(J,u1_incsp_1(A)) => ! [K] : ( m1_subset_1(K,u1_incsp_1(A)) => ! [L] : ( m1_subset_1(L,u2_incsp_1(A)) => ! [M] : ( m1_subset_1(M,u2_incsp_1(A)) => ! [N] : ( m1_subset_1(N,u2_incsp_1(A)) => ! [O] : ( m1_subset_1(O,u2_incsp_1(A)) => ! [P] : ( m1_subset_1(P,u2_incsp_1(A)) => ! [Q] : ( m1_subset_1(Q,u2_incsp_1(A)) => ! [R] : ( m1_subset_1(R,u2_incsp_1(A)) => ! [S] : ( m1_subset_1(S,u2_incsp_1(A)) => ! [T] : ( m1_subset_1(T,u2_incsp_1(A)) => ~ ( r4_incproj(A,B,C,L,D) & r4_incproj(A,B,F,M,E) & r4_incproj(A,B,H,N,G) & r4_incproj(A,H,F,O,K) & r4_incproj(A,H,I,P,D) & r4_incproj(A,F,J,Q,D) & r4_incproj(A,K,E,R,G) & r4_incproj(A,C,I,S,G) & r4_incproj(A,C,J,T,E) & r1_incproj(L,M,N) & B != H & B != C & B != E & F != E & ! [U] : ( m1_subset_1(U,u2_incsp_1(A)) => ~ r4_incproj(A,I,J,U,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(projred1,t14_projred1), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t21_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ( ~ r1_incsp_1(A,B,C) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ( r1_incsp_1(A,D,C) => k1_funct_1(k1_projred1(A,C,C,B),D) = D ) ) ) ) ) ) ), file(projred1,t21_projred1), []). fof(t22_funct_1,axiom,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(k5_relat_1(C,B))) => k1_funct_1(k5_relat_1(C,B),A) = k1_funct_1(B,k1_funct_1(C,A)) ) ) ) ), file(funct_1,t22_funct_1), []). fof(t22_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ( r1_incsp_1(A,C,D) => ( r1_incsp_1(A,B,D) | r1_incsp_1(A,B,E) | m1_subset_1(k1_funct_1(k1_projred1(A,D,E,B),C),u1_incsp_1(A)) ) ) ) ) ) ) ) ), file(projred1,t22_projred1), []). fof(t23_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u2_incsp_1(A)) => ( ( r1_incsp_1(A,C,E) & D = k1_funct_1(k1_projred1(A,E,F,B),C) ) => ( r1_incsp_1(A,B,E) | r1_incsp_1(A,B,F) | r1_incsp_1(A,D,F) ) ) ) ) ) ) ) ) ), file(projred1,t23_projred1), []). fof(t25_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u2_incsp_1(A)) => ~ ( ~ r1_incsp_1(A,B,D) & ~ r1_incsp_1(A,B,E) & ~ r1_incsp_1(A,C,E) & ~ r1_incsp_1(A,C,F) & ~ ( k1_relat_1(k5_relat_1(k1_projred1(A,D,E,B),k1_projred1(A,E,F,C))) = k4_relset_1(u1_incsp_1(A),u1_incsp_1(A),k1_projred1(A,D,E,B)) & k2_relat_1(k5_relat_1(k1_projred1(A,D,E,B),k1_projred1(A,E,F,C))) = k2_relat_1(k1_projred1(A,E,F,C)) ) ) ) ) ) ) ) ) ), file(projred1,t25_projred1), []). fof(t26_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ! [H] : ( m1_subset_1(H,u1_incsp_1(A)) => ( ( r1_incsp_1(A,E,C) & r1_incsp_1(A,F,C) & k1_funct_1(k1_projred1(A,C,D,B),E) = G & k1_funct_1(k1_projred1(A,C,D,B),F) = H & G = H ) => ( r1_incsp_1(A,B,C) | r1_incsp_1(A,B,D) | E = F ) ) ) ) ) ) ) ) ) ) ), file(projred1,t26_projred1), []). fof(t27_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ( ( r1_incsp_1(A,C,D) & r1_incsp_1(A,C,E) ) => ( r1_incsp_1(A,B,D) | r1_incsp_1(A,B,E) | k1_funct_1(k1_projred1(A,D,E,B),C) = C ) ) ) ) ) ) ) ), file(projred1,t27_projred1), []). fof(t2_subset,axiom,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), []). fof(t34_partfun1,axiom,( ! [A,B,C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & m2_relset_1(D,A,B) ) => ( ( k4_relset_1(A,B,C) = k4_relset_1(A,B,D) & ! [E] : ( m1_subset_1(E,A) => ( r2_hidden(E,k4_relset_1(A,B,C)) => k1_funct_1(C,E) = k1_funct_1(D,E) ) ) ) => C = D ) ) ) ), file(partfun1,t34_partfun1), []). fof(t3_subset,axiom,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), []). 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(t6_boole,axiom,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), []). fof(t7_boole,axiom,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), []). fof(t8_boole,axiom,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), []). fof(t8_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ? [E] : ( m1_subset_1(E,u1_incsp_1(A)) & r1_incsp_1(A,E,D) & E != B & E != C ) ) ) ) ) ), file(projred1,t8_projred1), []).