% Mizar ND problem: t5_afproj,afproj,79,51 fof(dh_c1_5__afproj,definition, ( ( ( ~ v3_struct_0(c1_5__afproj) & ~ v3_realset2(c1_5__afproj) & v1_diraf(c1_5__afproj) & l1_analoaf(c1_5__afproj) ) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,A,C) & r1_aff_4(c1_5__afproj,A,D) & r1_aff_4(c1_5__afproj,B,C) & r1_aff_4(c1_5__afproj,B,D) & v1_aff_1(A,c1_5__afproj) & v1_aff_1(B,c1_5__afproj) & v1_aff_4(C,c1_5__afproj) & v1_aff_4(D,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,A,B) | r1_aff_4(c1_5__afproj,C,D) ) ) ) ) ) ) ) => ! [E] : ( ( ~ v3_struct_0(E) & ~ v3_realset2(E) & v1_diraf(E) & l1_analoaf(E) ) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(E))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(E))) => ! [H] : ( m1_subset_1(H,k1_zfmisc_1(u1_struct_0(E))) => ! [I] : ( m1_subset_1(I,k1_zfmisc_1(u1_struct_0(E))) => ( ( r1_aff_4(E,F,H) & r1_aff_4(E,F,I) & r1_aff_4(E,G,H) & r1_aff_4(E,G,I) & v1_aff_1(F,E) & v1_aff_1(G,E) & v1_aff_4(H,E) & v1_aff_4(I,E) ) => ( r4_aff_1(E,F,G) | r1_aff_4(E,H,I) ) ) ) ) ) ) ) ), introduced(definition,[new_symbol(c1_5__afproj),file(afproj,c1_5__afproj)]), [interesting(0.8),axiom,file(afproj,c1_5__afproj)]). fof(dh_c2_5__afproj,definition, ( ( m1_subset_1(c2_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,B) & r1_aff_4(c1_5__afproj,c2_5__afproj,C) & r1_aff_4(c1_5__afproj,A,B) & r1_aff_4(c1_5__afproj,A,C) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(A,c1_5__afproj) & v1_aff_4(B,c1_5__afproj) & v1_aff_4(C,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,A) | r1_aff_4(c1_5__afproj,B,C) ) ) ) ) ) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,D,F) & r1_aff_4(c1_5__afproj,D,G) & r1_aff_4(c1_5__afproj,E,F) & r1_aff_4(c1_5__afproj,E,G) & v1_aff_1(D,c1_5__afproj) & v1_aff_1(E,c1_5__afproj) & v1_aff_4(F,c1_5__afproj) & v1_aff_4(G,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,D,E) | r1_aff_4(c1_5__afproj,F,G) ) ) ) ) ) ) ), introduced(definition,[new_symbol(c2_5__afproj),file(afproj,c2_5__afproj)]), [interesting(0.8),axiom,file(afproj,c2_5__afproj)]). fof(dh_c3_5__afproj,definition, ( ( m1_subset_1(c3_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,A) & r1_aff_4(c1_5__afproj,c2_5__afproj,B) & r1_aff_4(c1_5__afproj,c3_5__afproj,A) & r1_aff_4(c1_5__afproj,c3_5__afproj,B) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(A,c1_5__afproj) & v1_aff_4(B,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,A,B) ) ) ) ) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,D) & r1_aff_4(c1_5__afproj,c2_5__afproj,E) & r1_aff_4(c1_5__afproj,C,D) & r1_aff_4(c1_5__afproj,C,E) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(C,c1_5__afproj) & v1_aff_4(D,c1_5__afproj) & v1_aff_4(E,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,C) | r1_aff_4(c1_5__afproj,D,E) ) ) ) ) ) ), introduced(definition,[new_symbol(c3_5__afproj),file(afproj,c3_5__afproj)]), [interesting(0.8),axiom,file(afproj,c3_5__afproj)]). fof(dh_c4_5__afproj,definition, ( ( m1_subset_1(c4_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,A) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,A) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(A,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,c4_5__afproj,A) ) ) ) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,B) & r1_aff_4(c1_5__afproj,c2_5__afproj,C) & r1_aff_4(c1_5__afproj,c3_5__afproj,B) & r1_aff_4(c1_5__afproj,c3_5__afproj,C) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(B,c1_5__afproj) & v1_aff_4(C,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,B,C) ) ) ) ) ), introduced(definition,[new_symbol(c4_5__afproj),file(afproj,c4_5__afproj)]), [interesting(0.8),axiom,file(afproj,c4_5__afproj)]). fof(dh_c5_5__afproj,definition, ( ( m1_subset_1(c5_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,c5_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c5_5__afproj) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(c5_5__afproj,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,c4_5__afproj,c5_5__afproj) ) ) ) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,A) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,A) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(A,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,c4_5__afproj,A) ) ) ) ), introduced(definition,[new_symbol(c5_5__afproj),file(afproj,c5_5__afproj)]), [interesting(0.8),axiom,file(afproj,c5_5__afproj)]). fof(e1_5__afproj,assumption,( ~ r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) ), introduced(assumption,[file(afproj,e1_5__afproj)]), [interesting(0.8),axiom,file(afproj,e1_5__afproj)]). fof(e2_5__afproj,assumption, ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,c5_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c5_5__afproj) ), introduced(assumption,[file(afproj,e2_5__afproj)]), [interesting(0.8),axiom,file(afproj,e2_5__afproj)]). fof(e3_5__afproj,assumption, ( v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(c5_5__afproj,c1_5__afproj) ), introduced(assumption,[file(afproj,e3_5__afproj)]), [interesting(0.8),axiom,file(afproj,e3_5__afproj)]). fof(antisymmetry_r2_hidden,theorem,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), [interesting(0.9),axiom,file(hidden,r2_hidden)]). fof(dt_k1_xboole_0,axiom,( $true ), file(xboole_0,k1_xboole_0), [interesting(0.9),axiom,file(xboole_0,k1_xboole_0)]). fof(fc1_xboole_0,theorem,( v1_xboole_0(k1_xboole_0) ), file(xboole_0,fc1_xboole_0), [interesting(0.9),axiom,file(xboole_0,fc1_xboole_0)]). fof(t1_subset,theorem,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), [interesting(0.9),axiom,file(subset,t1_subset)]). fof(t4_subset,theorem,( ! [A,B,C] : ( ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) ) => m1_subset_1(A,C) ) ), file(subset,t4_subset), [interesting(0.9),axiom,file(subset,t4_subset)]). fof(t5_subset,theorem,( ! [A,B,C] : ~ ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) & v1_xboole_0(C) ) ), file(subset,t5_subset), [interesting(0.9),axiom,file(subset,t5_subset)]). fof(existence_l1_struct_0,axiom,( ? [A] : l1_struct_0(A) ), file(struct_0,l1_struct_0), [interesting(0.9),axiom,file(struct_0,l1_struct_0)]). fof(dt_l1_struct_0,axiom,( $true ), file(struct_0,l1_struct_0), [interesting(0.9),axiom,file(struct_0,l1_struct_0)]). fof(dh_c6_5__afproj,definition, ( ? [A] : m1_subset_1(A,c4_5__afproj) => m1_subset_1(c6_5__afproj,c4_5__afproj) ), introduced(definition,[new_symbol(c6_5__afproj),file(afproj,c6_5__afproj)]), [interesting(0.8),axiom,file(afproj,c6_5__afproj)]). fof(t8_boole,theorem,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), [interesting(0.9),axiom,file(boole,t8_boole)]). fof(reflexivity_r1_tarski,theorem,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), [interesting(0.9),axiom,file(tarski,r1_tarski)]). fof(existence_l1_analoaf,axiom,( ? [A] : l1_analoaf(A) ), file(analoaf,l1_analoaf), [interesting(0.9),axiom,file(analoaf,l1_analoaf)]). fof(dt_l1_analoaf,axiom,( ! [A] : ( l1_analoaf(A) => l1_struct_0(A) ) ), file(analoaf,l1_analoaf), [interesting(0.9),axiom,file(analoaf,l1_analoaf)]). fof(fc1_struct_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ~ v1_xboole_0(u1_struct_0(A)) ) ), file(struct_0,fc1_struct_0), [interesting(0.9),axiom,file(struct_0,fc1_struct_0)]). fof(rc1_subset_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_xboole_0(B) ) ) ), file(subset_1,rc1_subset_1), [interesting(0.9),axiom,file(subset_1,rc1_subset_1)]). fof(rc1_xboole_0,theorem,( ? [A] : v1_xboole_0(A) ), file(xboole_0,rc1_xboole_0), [interesting(0.9),axiom,file(xboole_0,rc1_xboole_0)]). fof(rc2_subset_1,theorem,( ! [A] : ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & v1_xboole_0(B) ) ), file(subset_1,rc2_subset_1), [interesting(0.9),axiom,file(subset_1,rc2_subset_1)]). fof(rc2_xboole_0,theorem,( ? [A] : ~ v1_xboole_0(A) ), file(xboole_0,rc2_xboole_0), [interesting(0.9),axiom,file(xboole_0,rc2_xboole_0)]). fof(rc3_struct_0,theorem,( ? [A] : ( l1_struct_0(A) & ~ v3_struct_0(A) ) ), file(struct_0,rc3_struct_0), [interesting(0.9),axiom,file(struct_0,rc3_struct_0)]). fof(rc5_struct_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & ~ v1_xboole_0(B) ) ) ), file(struct_0,rc5_struct_0), [interesting(0.9),axiom,file(struct_0,rc5_struct_0)]). fof(t2_subset,theorem,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), [interesting(0.9),axiom,file(subset,t2_subset)]). fof(t6_boole,theorem,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), [interesting(0.9),axiom,file(boole,t6_boole)]). fof(t7_boole,theorem,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), [interesting(0.9),axiom,file(boole,t7_boole)]). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), [interesting(0.9),axiom,file(zfmisc_1,k1_zfmisc_1)]). fof(dt_u1_struct_0,axiom,( $true ), file(struct_0,u1_struct_0), [interesting(0.9),axiom,file(struct_0,u1_struct_0)]). fof(dt_c1_5__afproj,assumption, ( ~ v3_struct_0(c1_5__afproj) & ~ v3_realset2(c1_5__afproj) & v1_diraf(c1_5__afproj) & l1_analoaf(c1_5__afproj) ), introduced(assumption,[file(afproj,c1_5__afproj)]), [interesting(0.8),axiom,file(afproj,c1_5__afproj)]). fof(fc1_subset_1,theorem,( ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ), file(subset_1,fc1_subset_1), [interesting(0.9),axiom,file(subset_1,fc1_subset_1)]). fof(t3_subset,theorem,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), [interesting(0.9),axiom,file(subset,t3_subset)]). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), [interesting(0.9),axiom,file(subset_1,m1_subset_1)]). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), [interesting(0.9),axiom,file(subset_1,m1_subset_1)]). fof(dt_c4_5__afproj,assumption,( m1_subset_1(c4_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) ), introduced(assumption,[file(afproj,c4_5__afproj)]), [interesting(0.8),axiom,file(afproj,c4_5__afproj)]). fof(e5_5__afproj,plain,( ? [A] : m1_subset_1(A,c4_5__afproj) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c4_5__afproj])],[antisymmetry_r2_hidden,dt_k1_xboole_0,fc1_xboole_0,t1_subset,t4_subset,t5_subset,t8_boole,reflexivity_r1_tarski,existence_l1_analoaf,existence_l1_struct_0,dt_l1_analoaf,dt_l1_struct_0,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t6_boole,t7_boole,dt_k1_zfmisc_1,dt_u1_struct_0,dt_c1_5__afproj,fc1_subset_1,t3_subset,existence_m1_subset_1,dt_m1_subset_1,dt_c4_5__afproj]), [interesting(0.8),file(afproj,e5_5__afproj),[file(afproj,e5_5__afproj)]]). fof(dt_c6_5__afproj,plain,( m1_subset_1(c6_5__afproj,c4_5__afproj) ), inference(consider,[status(thm),assumptions([dt_c1_5__afproj,dt_c4_5__afproj])],[dh_c6_5__afproj,e5_5__afproj]), [interesting(0.8),file(afproj,c6_5__afproj),[file(afproj,c6_5__afproj)]]). fof(dh_c7_5__afproj,definition, ( ? [A] : m1_subset_1(A,c5_5__afproj) => m1_subset_1(c7_5__afproj,c5_5__afproj) ), introduced(definition,[new_symbol(c7_5__afproj),file(afproj,c7_5__afproj)]), [interesting(0.8),axiom,file(afproj,c7_5__afproj)]). fof(dt_c5_5__afproj,assumption,( m1_subset_1(c5_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) ), introduced(assumption,[file(afproj,c5_5__afproj)]), [interesting(0.8),axiom,file(afproj,c5_5__afproj)]). fof(e6_5__afproj,plain,( ? [A] : m1_subset_1(A,c5_5__afproj) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c5_5__afproj])],[antisymmetry_r2_hidden,dt_k1_xboole_0,fc1_xboole_0,t1_subset,t4_subset,t5_subset,t8_boole,reflexivity_r1_tarski,existence_l1_analoaf,existence_l1_struct_0,dt_l1_analoaf,dt_l1_struct_0,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t6_boole,t7_boole,dt_k1_zfmisc_1,dt_u1_struct_0,dt_c1_5__afproj,fc1_subset_1,t3_subset,existence_m1_subset_1,dt_m1_subset_1,dt_c5_5__afproj]), [interesting(0.8),file(afproj,e6_5__afproj),[file(afproj,e6_5__afproj)]]). fof(dt_c7_5__afproj,plain,( m1_subset_1(c7_5__afproj,c5_5__afproj) ), inference(consider,[status(thm),assumptions([dt_c1_5__afproj,dt_c5_5__afproj])],[dh_c7_5__afproj,e6_5__afproj]), [interesting(0.8),file(afproj,c7_5__afproj),[file(afproj,c7_5__afproj)]]). fof(symmetry_r4_aff_1,theorem,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => ( r4_aff_1(A,B,C) => r4_aff_1(A,C,B) ) ) ), file(aff_1,r4_aff_1), [interesting(0.9),axiom,file(aff_1,r4_aff_1)]). fof(redefinition_r4_aff_1,definition,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => ( r4_aff_1(A,B,C) <=> r3_aff_1(A,B,C) ) ) ), file(aff_1,r4_aff_1), [interesting(0.9),axiom,file(aff_1,r4_aff_1)]). fof(dt_k2_aff_4,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => m1_subset_1(k2_aff_4(A,B,C),k1_zfmisc_1(u1_struct_0(A))) ) ), file(aff_4,k2_aff_4), [interesting(0.9),axiom,file(aff_4,k2_aff_4)]). fof(dt_c2_5__afproj,assumption,( m1_subset_1(c2_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) ), introduced(assumption,[file(afproj,c2_5__afproj)]), [interesting(0.8),axiom,file(afproj,c2_5__afproj)]). fof(dt_c3_5__afproj,assumption,( m1_subset_1(c3_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) ), introduced(assumption,[file(afproj,c3_5__afproj)]), [interesting(0.8),axiom,file(afproj,c3_5__afproj)]). fof(de_c8_5__afproj,definition,( c8_5__afproj = c6_5__afproj ), introduced(definition,[new_symbol(c8_5__afproj),file(afproj,c8_5__afproj)]), [interesting(0.8),axiom,file(afproj,c8_5__afproj)]). fof(t59_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ~ ( v1_aff_4(B,A) & B = k1_xboole_0 ) ) ) ), file(aff_4,t59_aff_4), [interesting(0.9),axiom,file(aff_4,t59_aff_4)]). fof(e4_5__afproj,plain, ( c4_5__afproj != k1_xboole_0 & c5_5__afproj != k1_xboole_0 ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[antisymmetry_r2_hidden,t1_subset,t4_subset,t5_subset,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t7_boole,t8_boole,existence_l1_analoaf,existence_m1_subset_1,dt_k1_xboole_0,dt_k1_zfmisc_1,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,fc1_subset_1,fc1_xboole_0,t3_subset,t6_boole,e3_5__afproj,t59_aff_4]), [interesting(0.8),file(afproj,e4_5__afproj),[file(afproj,e4_5__afproj)]]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.9),axiom,file(tarski,d3_tarski)]). fof(e7_5__afproj,plain, ( m1_subset_1(c6_5__afproj,u1_struct_0(c1_5__afproj)) & m1_subset_1(c7_5__afproj,u1_struct_0(c1_5__afproj)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[existence_l1_analoaf,existence_l1_struct_0,dt_k1_zfmisc_1,dt_l1_analoaf,dt_l1_struct_0,fc1_struct_0,fc1_subset_1,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t4_subset,t5_subset,t8_boole,reflexivity_r1_tarski,antisymmetry_r2_hidden,existence_m1_subset_1,dt_k1_xboole_0,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,dt_c6_5__afproj,dt_c7_5__afproj,fc1_xboole_0,t1_subset,t3_subset,t6_boole,t7_boole,e4_5__afproj,d3_tarski]), [interesting(0.8),file(afproj,e7_5__afproj),[file(afproj,e7_5__afproj)]]). fof(dt_c8_5__afproj,plain,( m1_subset_1(c8_5__afproj,u1_struct_0(c1_5__afproj)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,fc1_xboole_0,t1_subset,t4_subset,t5_subset,dt_k1_zfmisc_1,fc1_subset_1,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc5_struct_0,t2_subset,t3_subset,t6_boole,t7_boole,t8_boole,existence_l1_analoaf,existence_l1_struct_0,dt_l1_analoaf,dt_l1_struct_0,dt_c4_5__afproj,dt_c5_5__afproj,fc1_struct_0,rc3_struct_0,existence_m1_subset_1,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c6_5__afproj,dt_c7_5__afproj,de_c8_5__afproj,e7_5__afproj]), [interesting(0.8),file(afproj,c8_5__afproj),[file(afproj,c8_5__afproj)]]). fof(de_c9_5__afproj,definition,( c9_5__afproj = c7_5__afproj ), introduced(definition,[new_symbol(c9_5__afproj),file(afproj,c9_5__afproj)]), [interesting(0.8),axiom,file(afproj,c9_5__afproj)]). fof(dt_c9_5__afproj,plain,( m1_subset_1(c9_5__afproj,u1_struct_0(c1_5__afproj)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,fc1_xboole_0,t1_subset,t4_subset,t5_subset,dt_k1_zfmisc_1,fc1_subset_1,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc5_struct_0,t2_subset,t3_subset,t6_boole,t7_boole,t8_boole,existence_l1_analoaf,existence_l1_struct_0,dt_l1_analoaf,dt_l1_struct_0,dt_c4_5__afproj,dt_c5_5__afproj,fc1_struct_0,rc3_struct_0,existence_m1_subset_1,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c6_5__afproj,dt_c7_5__afproj,de_c9_5__afproj,e7_5__afproj]), [interesting(0.8),file(afproj,c9_5__afproj),[file(afproj,c9_5__afproj)]]). fof(d3_aff_4,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( v1_aff_1(C,A) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( D = k2_aff_4(A,B,C) <=> ( r2_hidden(B,D) & r4_aff_1(A,C,D) ) ) ) ) ) ) ) ), file(aff_4,d3_aff_4), [interesting(0.9),axiom,file(aff_4,d3_aff_4)]). fof(e10_5__afproj,plain, ( r4_aff_1(c1_5__afproj,c2_5__afproj,k2_aff_4(c1_5__afproj,c8_5__afproj,c2_5__afproj)) & r4_aff_1(c1_5__afproj,c2_5__afproj,k2_aff_4(c1_5__afproj,c9_5__afproj,c2_5__afproj)) & r4_aff_1(c1_5__afproj,c3_5__afproj,k2_aff_4(c1_5__afproj,c8_5__afproj,c3_5__afproj)) & r4_aff_1(c1_5__afproj,c3_5__afproj,k2_aff_4(c1_5__afproj,c9_5__afproj,c3_5__afproj)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[dt_k1_xboole_0,fc1_xboole_0,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,dt_c6_5__afproj,dt_c7_5__afproj,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t5_subset,t6_boole,t8_boole,antisymmetry_r2_hidden,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_k2_aff_4,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,dt_c8_5__afproj,dt_c9_5__afproj,de_c8_5__afproj,de_c9_5__afproj,fc1_subset_1,t1_subset,t3_subset,t4_subset,t7_boole,e3_5__afproj,d3_aff_4]), [interesting(0.8),file(afproj,e10_5__afproj),[file(afproj,e10_5__afproj)]]). fof(t58_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ~ ( ~ ( r4_aff_1(A,B,C) & r4_aff_1(A,C,D) ) & ~ ( r4_aff_1(A,B,C) & r4_aff_1(A,D,C) ) & ~ ( r4_aff_1(A,C,B) & r4_aff_1(A,C,D) ) & ~ ( r4_aff_1(A,C,B) & r4_aff_1(A,D,C) ) ) => r4_aff_1(A,B,D) ) ) ) ) ) ), file(aff_1,t58_aff_1), [interesting(0.9),axiom,file(aff_1,t58_aff_1)]). fof(e12_5__afproj,plain, ( r4_aff_1(c1_5__afproj,k2_aff_4(c1_5__afproj,c8_5__afproj,c2_5__afproj),k2_aff_4(c1_5__afproj,c9_5__afproj,c2_5__afproj)) & r4_aff_1(c1_5__afproj,k2_aff_4(c1_5__afproj,c8_5__afproj,c3_5__afproj),k2_aff_4(c1_5__afproj,c9_5__afproj,c3_5__afproj)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[antisymmetry_r2_hidden,dt_k1_xboole_0,dt_c4_5__afproj,dt_c5_5__afproj,fc1_xboole_0,t1_subset,t4_subset,t5_subset,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,dt_c6_5__afproj,dt_c7_5__afproj,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t6_boole,t7_boole,t8_boole,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_k2_aff_4,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c8_5__afproj,dt_c9_5__afproj,de_c8_5__afproj,de_c9_5__afproj,fc1_subset_1,t3_subset,e10_5__afproj,t58_aff_1]), [interesting(0.8),file(afproj,e12_5__afproj),[file(afproj,e12_5__afproj)]]). fof(dt_k3_aff_4,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => m1_subset_1(k3_aff_4(A,B,C),k1_zfmisc_1(u1_struct_0(A))) ) ), file(aff_4,k3_aff_4), [interesting(0.9),axiom,file(aff_4,k3_aff_4)]). fof(t68_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(C,A) & v1_aff_4(D,A) & r1_aff_4(A,C,D) ) => r1_tarski(k2_aff_4(A,B,C),k3_aff_4(A,B,D)) ) ) ) ) ) ), file(aff_4,t68_aff_4), [interesting(0.9),axiom,file(aff_4,t68_aff_4)]). fof(e8_5__afproj,plain, ( r1_tarski(k2_aff_4(c1_5__afproj,c8_5__afproj,c2_5__afproj),k3_aff_4(c1_5__afproj,c8_5__afproj,c4_5__afproj)) & r1_tarski(k2_aff_4(c1_5__afproj,c8_5__afproj,c3_5__afproj),k3_aff_4(c1_5__afproj,c8_5__afproj,c4_5__afproj)) & r1_tarski(k2_aff_4(c1_5__afproj,c9_5__afproj,c2_5__afproj),k3_aff_4(c1_5__afproj,c9_5__afproj,c5_5__afproj)) & r1_tarski(k2_aff_4(c1_5__afproj,c9_5__afproj,c3_5__afproj),k3_aff_4(c1_5__afproj,c9_5__afproj,c5_5__afproj)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e2_5__afproj,e3_5__afproj])],[antisymmetry_r2_hidden,dt_k1_xboole_0,fc1_xboole_0,t1_subset,t4_subset,t5_subset,existence_l1_struct_0,dt_l1_struct_0,dt_c6_5__afproj,dt_c7_5__afproj,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t6_boole,t7_boole,t8_boole,reflexivity_r1_tarski,existence_l1_analoaf,existence_m1_subset_1,dt_k1_zfmisc_1,dt_k2_aff_4,dt_k3_aff_4,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,dt_c8_5__afproj,dt_c9_5__afproj,de_c8_5__afproj,de_c9_5__afproj,fc1_subset_1,t3_subset,e2_5__afproj,e3_5__afproj,t68_aff_4]), [interesting(0.8),file(afproj,e8_5__afproj),[file(afproj,e8_5__afproj)]]). fof(t66_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( v1_aff_4(C,A) => ( r2_hidden(B,C) <=> k3_aff_4(A,B,C) = C ) ) ) ) ) ), file(aff_4,t66_aff_4), [interesting(0.9),axiom,file(aff_4,t66_aff_4)]). fof(e9_5__afproj,plain, ( r1_tarski(k2_aff_4(c1_5__afproj,c8_5__afproj,c2_5__afproj),c4_5__afproj) & r1_tarski(k2_aff_4(c1_5__afproj,c8_5__afproj,c3_5__afproj),c4_5__afproj) & r1_tarski(k2_aff_4(c1_5__afproj,c9_5__afproj,c2_5__afproj),c5_5__afproj) & r1_tarski(k2_aff_4(c1_5__afproj,c9_5__afproj,c3_5__afproj),c5_5__afproj) ), inference(mizar_by,[status(thm),assumptions([e2_5__afproj,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[existence_l1_struct_0,dt_l1_struct_0,dt_c6_5__afproj,dt_c7_5__afproj,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t5_subset,t8_boole,reflexivity_r1_tarski,antisymmetry_r2_hidden,existence_l1_analoaf,existence_m1_subset_1,dt_k1_xboole_0,dt_k1_zfmisc_1,dt_k2_aff_4,dt_k3_aff_4,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,dt_c8_5__afproj,dt_c9_5__afproj,de_c8_5__afproj,de_c9_5__afproj,fc1_subset_1,fc1_xboole_0,t1_subset,t3_subset,t4_subset,t6_boole,t7_boole,e8_5__afproj,e3_5__afproj,e4_5__afproj,t66_aff_4]), [interesting(0.8),file(afproj,e9_5__afproj),[file(afproj,e9_5__afproj)]]). fof(e1_5_1__afproj,assumption,( r4_aff_1(c1_5__afproj,k2_aff_4(c1_5__afproj,c8_5__afproj,c2_5__afproj),k2_aff_4(c1_5__afproj,c8_5__afproj,c3_5__afproj)) ), introduced(assumption,[file(afproj,e1_5_1__afproj)]), [interesting(0.65),axiom,file(afproj,e1_5_1__afproj)]). fof(e2_5_1__afproj,plain,( r4_aff_1(c1_5__afproj,k2_aff_4(c1_5__afproj,c8_5__afproj,c2_5__afproj),c3_5__afproj) ), inference(mizar_by,[status(thm),assumptions([e1_5_1__afproj,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[antisymmetry_r2_hidden,dt_k1_xboole_0,dt_c4_5__afproj,dt_c5_5__afproj,fc1_xboole_0,t1_subset,t4_subset,t5_subset,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,dt_c6_5__afproj,dt_c7_5__afproj,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t6_boole,t7_boole,t8_boole,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_k2_aff_4,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c8_5__afproj,dt_c9_5__afproj,de_c8_5__afproj,de_c9_5__afproj,fc1_subset_1,t3_subset,e1_5_1__afproj,e10_5__afproj,t58_aff_1]), [interesting(0.65),file(afproj,e2_5_1__afproj),[file(afproj,e2_5_1__afproj)]]). fof(e3_5_1__afproj,plain,( ~ $true ), inference(mizar_by,[status(thm),assumptions([e1_5_1__afproj,e1_5__afproj,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[antisymmetry_r2_hidden,dt_k1_xboole_0,dt_c4_5__afproj,dt_c5_5__afproj,fc1_xboole_0,t1_subset,t4_subset,t5_subset,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,dt_c6_5__afproj,dt_c7_5__afproj,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t6_boole,t7_boole,t8_boole,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_k2_aff_4,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c8_5__afproj,dt_c9_5__afproj,de_c8_5__afproj,de_c9_5__afproj,fc1_subset_1,t3_subset,e2_5_1__afproj,e1_5__afproj,e10_5__afproj,t58_aff_1]), [interesting(0.65),file(afproj,e3_5_1__afproj),[file(afproj,e3_5_1__afproj)]]). fof(i2_5_1__afproj,theorem,( $true ), introduced(tautology,[file(afproj,i2_5_1__afproj)]), [interesting(0.65),trivial,file(afproj,i2_5_1__afproj)]). fof(i1_5_1__afproj,plain,( ~ $true ), inference(conclusion,[status(thm),assumptions([e1_5_1__afproj,e1_5__afproj,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[e3_5_1__afproj,i2_5_1__afproj]), [interesting(0.65),file(afproj,i1_5_1__afproj),[file(afproj,i1_5_1__afproj)]]). fof(e11_5__afproj,plain,( ~ r4_aff_1(c1_5__afproj,k2_aff_4(c1_5__afproj,c8_5__afproj,c2_5__afproj),k2_aff_4(c1_5__afproj,c8_5__afproj,c3_5__afproj)) ), inference(discharge_asm,[status(thm),assumptions([e1_5__afproj,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj]),discharge_asm(discharge,[e1_5_1__afproj])],[e1_5_1__afproj,i1_5_1__afproj]), [interesting(0.8),file(afproj,e11_5__afproj),[file(afproj,e11_5__afproj)]]). fof(t55_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_4(B,A) & v1_aff_4(C,A) ) => ( r1_aff_4(A,B,C) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & ? [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) & ? [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) & ? [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) & ~ r4_aff_1(A,D,E) & r1_tarski(D,B) & r1_tarski(E,B) & r1_tarski(F,C) & r1_tarski(G,C) & ( r4_aff_1(A,D,F) | r4_aff_1(A,F,D) ) & ( r4_aff_1(A,E,G) | r4_aff_1(A,G,E) ) ) ) ) ) ) ) ) ) ) ), file(aff_4,t55_aff_4), [interesting(0.9),axiom,file(aff_4,t55_aff_4)]). fof(e13_5__afproj,plain,( r1_aff_4(c1_5__afproj,c4_5__afproj,c5_5__afproj) ), inference(mizar_by,[status(thm),assumptions([e2_5__afproj,e1_5__afproj,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[antisymmetry_r2_hidden,dt_k1_xboole_0,fc1_xboole_0,t1_subset,t4_subset,t5_subset,existence_l1_struct_0,dt_l1_struct_0,dt_c6_5__afproj,dt_c7_5__afproj,fc1_struct_0,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t6_boole,t7_boole,t8_boole,reflexivity_r1_tarski,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_k2_aff_4,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,dt_c8_5__afproj,dt_c9_5__afproj,de_c8_5__afproj,de_c9_5__afproj,fc1_subset_1,t3_subset,e12_5__afproj,e3_5__afproj,e9_5__afproj,e11_5__afproj,t55_aff_4]), [interesting(0.8),file(afproj,e13_5__afproj),[file(afproj,e13_5__afproj)]]). fof(i7_5__afproj,theorem,( $true ), introduced(tautology,[file(afproj,i7_5__afproj)]), [interesting(0.8),trivial,file(afproj,i7_5__afproj)]). fof(i6_5__afproj,plain,( r1_aff_4(c1_5__afproj,c4_5__afproj,c5_5__afproj) ), inference(conclusion,[status(thm),assumptions([e2_5__afproj,e1_5__afproj,dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj,e3_5__afproj])],[e13_5__afproj,i7_5__afproj]), [interesting(0.8),file(afproj,i6_5__afproj),[file(afproj,i6_5__afproj)]]). fof(i5_5__afproj,plain, ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,c5_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c5_5__afproj) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(c5_5__afproj,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,c4_5__afproj,c5_5__afproj) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj,dt_c5_5__afproj]),discharge_asm(discharge,[e1_5__afproj,e2_5__afproj,e3_5__afproj])],[e1_5__afproj,e2_5__afproj,e3_5__afproj,i6_5__afproj]), [interesting(0.8),file(afproj,i5_5__afproj),[file(afproj,i5_5__afproj)]]). fof(i5_5_tmp__afproj,plain, ( m1_subset_1(c5_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,c5_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,c5_5__afproj) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(c5_5__afproj,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,c4_5__afproj,c5_5__afproj) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj]),discharge_asm(discharge,[dt_c5_5__afproj])],[dt_c5_5__afproj,i5_5__afproj]), [interesting(0.8),i4_5__afproj]). fof(i4_5__afproj,plain,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,A) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,A) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(A,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,c4_5__afproj,A) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj,dt_c4_5__afproj])],[i5_5_tmp__afproj,dh_c5_5__afproj]), [interesting(0.8),file(afproj,i4_5__afproj),[file(afproj,i4_5__afproj)]]). fof(i4_5_tmp__afproj,plain, ( m1_subset_1(c4_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c2_5__afproj,A) & r1_aff_4(c1_5__afproj,c3_5__afproj,c4_5__afproj) & r1_aff_4(c1_5__afproj,c3_5__afproj,A) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(c4_5__afproj,c1_5__afproj) & v1_aff_4(A,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,c4_5__afproj,A) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj]),discharge_asm(discharge,[dt_c4_5__afproj])],[dt_c4_5__afproj,i4_5__afproj]), [interesting(0.8),i3_5__afproj]). fof(i3_5__afproj,plain,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,A) & r1_aff_4(c1_5__afproj,c2_5__afproj,B) & r1_aff_4(c1_5__afproj,c3_5__afproj,A) & r1_aff_4(c1_5__afproj,c3_5__afproj,B) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(A,c1_5__afproj) & v1_aff_4(B,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,A,B) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj,dt_c3_5__afproj])],[i4_5_tmp__afproj,dh_c4_5__afproj]), [interesting(0.8),file(afproj,i3_5__afproj),[file(afproj,i3_5__afproj)]]). fof(i3_5_tmp__afproj,plain, ( m1_subset_1(c3_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,A) & r1_aff_4(c1_5__afproj,c2_5__afproj,B) & r1_aff_4(c1_5__afproj,c3_5__afproj,A) & r1_aff_4(c1_5__afproj,c3_5__afproj,B) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(c3_5__afproj,c1_5__afproj) & v1_aff_4(A,c1_5__afproj) & v1_aff_4(B,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,c3_5__afproj) | r1_aff_4(c1_5__afproj,A,B) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj]),discharge_asm(discharge,[dt_c3_5__afproj])],[dt_c3_5__afproj,i3_5__afproj]), [interesting(0.8),i2_5__afproj]). fof(i2_5__afproj,plain,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,B) & r1_aff_4(c1_5__afproj,c2_5__afproj,C) & r1_aff_4(c1_5__afproj,A,B) & r1_aff_4(c1_5__afproj,A,C) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(A,c1_5__afproj) & v1_aff_4(B,c1_5__afproj) & v1_aff_4(C,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,A) | r1_aff_4(c1_5__afproj,B,C) ) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_5__afproj,dt_c2_5__afproj])],[i3_5_tmp__afproj,dh_c3_5__afproj]), [interesting(0.8),file(afproj,i2_5__afproj),[file(afproj,i2_5__afproj)]]). fof(i2_5_tmp__afproj,plain, ( m1_subset_1(c2_5__afproj,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,c2_5__afproj,B) & r1_aff_4(c1_5__afproj,c2_5__afproj,C) & r1_aff_4(c1_5__afproj,A,B) & r1_aff_4(c1_5__afproj,A,C) & v1_aff_1(c2_5__afproj,c1_5__afproj) & v1_aff_1(A,c1_5__afproj) & v1_aff_4(B,c1_5__afproj) & v1_aff_4(C,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,c2_5__afproj,A) | r1_aff_4(c1_5__afproj,B,C) ) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_5__afproj]),discharge_asm(discharge,[dt_c2_5__afproj])],[dt_c2_5__afproj,i2_5__afproj]), [interesting(0.8),i1_5__afproj]). fof(i1_5__afproj,plain,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,A,C) & r1_aff_4(c1_5__afproj,A,D) & r1_aff_4(c1_5__afproj,B,C) & r1_aff_4(c1_5__afproj,B,D) & v1_aff_1(A,c1_5__afproj) & v1_aff_1(B,c1_5__afproj) & v1_aff_4(C,c1_5__afproj) & v1_aff_4(D,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,A,B) | r1_aff_4(c1_5__afproj,C,D) ) ) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_5__afproj])],[i2_5_tmp__afproj,dh_c2_5__afproj]), [interesting(0.8),file(afproj,i1_5__afproj),[file(afproj,i1_5__afproj)]]). fof(i1_5_tmp__afproj,plain, ( ( ~ v3_struct_0(c1_5__afproj) & ~ v3_realset2(c1_5__afproj) & v1_diraf(c1_5__afproj) & l1_analoaf(c1_5__afproj) ) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_5__afproj))) => ( ( r1_aff_4(c1_5__afproj,A,C) & r1_aff_4(c1_5__afproj,A,D) & r1_aff_4(c1_5__afproj,B,C) & r1_aff_4(c1_5__afproj,B,D) & v1_aff_1(A,c1_5__afproj) & v1_aff_1(B,c1_5__afproj) & v1_aff_4(C,c1_5__afproj) & v1_aff_4(D,c1_5__afproj) ) => ( r4_aff_1(c1_5__afproj,A,B) | r1_aff_4(c1_5__afproj,C,D) ) ) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_5__afproj])],[dt_c1_5__afproj,i1_5__afproj]), [interesting(1),t5_afproj]). fof(t5_afproj,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( ( r1_aff_4(A,B,D) & r1_aff_4(A,B,E) & r1_aff_4(A,C,D) & r1_aff_4(A,C,E) & v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_4(D,A) & v1_aff_4(E,A) ) => ( r4_aff_1(A,B,C) | r1_aff_4(A,D,E) ) ) ) ) ) ) ) ), inference(let,[status(thm),assumptions([])],[i1_5_tmp__afproj,dh_c1_5__afproj]), [interesting(1),file(afproj,t5_afproj),[file(afproj,t5_afproj)]]).