% Mizar problem: t8_conmetr1,conmetr1,578,44 fof(t8_conmetr1,conjecture,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) <=> v3_conmetr1(A) ) ) ), inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,d1_aff_1,d3_conmetr1,d4_aff_2,dt_k1_zfmisc_1,dt_l1_analoaf,dt_l1_struct_0,dt_m1_subset_1,dt_u1_struct_0,existence_l1_analoaf,existence_l1_struct_0,existence_m1_subset_1,redefinition_r4_aff_1,reflexivity_r1_tarski,symmetry_r4_aff_1,t11_aff_1,t12_aff_1,t13_aff_1,t14_aff_1,t15_aff_1,t16_aff_1,t17_aff_2,t1_subset,t21_aff_2,t23_aff_1,t26_aff_2,t27_aff_2,t2_conmetr1,t33_aff_1,t39_aff_1,t3_subset,t47_diraf,t4_subset,t53_aff_1,t55_aff_1,t59_aff_1,t62_aff_1,t65_aff_1,t66_aff_1,t67_aff_1,t6_conmetr1,t74_aff_1,t7_conmetr1]), [file(conmetr1,t8_conmetr1)]). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(d1_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) <=> r2_analoaf(A,B,C,B,D) ) ) ) ) ) ), file(aff_1,d1_aff_1), []). fof(d3_conmetr1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v3_conmetr1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,k1_zfmisc_1(u1_struct_0(A))) => ! [K] : ( m1_subset_1(K,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(J,A) & v1_aff_1(K,A) & r2_hidden(B,J) & r2_hidden(D,J) & r2_hidden(F,J) & r2_hidden(H,J) & r2_hidden(C,K) & r2_hidden(E,K) & r2_hidden(G,K) & r2_hidden(I,K) & r2_analoaf(A,D,C,H,G) & r2_analoaf(A,C,B,G,F) & r2_analoaf(A,B,E,F,I) ) => ( r2_hidden(E,J) | r2_hidden(C,J) | r2_hidden(G,J) | r2_hidden(I,J) | r2_hidden(B,K) | r2_hidden(D,K) | r2_hidden(F,K) | r2_hidden(H,K) | r2_analoaf(A,D,E,H,I) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(conmetr1,d3_conmetr1), []). fof(d4_aff_2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(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,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( r2_hidden(E,B) & r2_hidden(E,C) & r2_hidden(E,D) & r2_hidden(F,B) & r2_hidden(I,B) & r2_hidden(G,C) & r2_hidden(J,C) & r2_hidden(H,D) & r2_hidden(K,D) & v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_analoaf(A,F,G,I,J) & r2_analoaf(A,F,H,I,K) ) => ( E = F | E = G | E = H | B = C | B = D | r2_analoaf(A,G,H,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d4_aff_2), []). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), []). fof(dt_l1_analoaf,axiom,( ! [A] : ( l1_analoaf(A) => l1_struct_0(A) ) ), file(analoaf,l1_analoaf), []). fof(dt_l1_struct_0,axiom,( $true ), file(struct_0,l1_struct_0), []). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), []). fof(dt_u1_struct_0,axiom,( $true ), file(struct_0,u1_struct_0), []). fof(existence_l1_analoaf,axiom,( ? [A] : l1_analoaf(A) ), file(analoaf,l1_analoaf), []). fof(existence_l1_struct_0,axiom,( ? [A] : l1_struct_0(A) ), file(struct_0,l1_struct_0), []). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), []). fof(redefinition_r4_aff_1,axiom,( ! [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), []). fof(reflexivity_r1_tarski,axiom,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), []). fof(symmetry_r4_aff_1,axiom,( ! [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), []). fof(t11_aff_1,axiom,( ! [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,u1_struct_0(A)) => ( r2_analoaf(A,B,C,C,B) & r2_analoaf(A,B,C,B,C) ) ) ) ) ), file(aff_1,t11_aff_1), []). fof(t12_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,D) & r2_analoaf(A,D,D,B,C) ) ) ) ) ) ), file(aff_1,t12_aff_1), []). fof(t13_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,E) => ( r2_analoaf(A,B,C,E,D) & r2_analoaf(A,C,B,D,E) & r2_analoaf(A,C,B,E,D) & r2_analoaf(A,D,E,B,C) & r2_analoaf(A,D,E,C,B) & r2_analoaf(A,E,D,B,C) & r2_analoaf(A,E,D,C,B) ) ) ) ) ) ) ) ), file(aff_1,t13_aff_1), []). fof(t14_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( B != C & ~ ( ~ ( r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,C,F,G) ) & ~ ( r2_analoaf(A,B,C,D,E) & r2_analoaf(A,F,G,B,C) ) & ~ ( r2_analoaf(A,D,E,B,C) & r2_analoaf(A,F,G,B,C) ) & ~ ( r2_analoaf(A,D,E,B,C) & r2_analoaf(A,B,C,F,G) ) ) & ~ r2_analoaf(A,D,E,F,G) ) ) ) ) ) ) ) ) ), file(aff_1,t14_aff_1), []). fof(t15_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) => ( r1_aff_1(A,B,D,C) & r1_aff_1(A,C,B,D) & r1_aff_1(A,C,D,B) & r1_aff_1(A,D,B,C) & r1_aff_1(A,D,C,B) ) ) ) ) ) ) ), file(aff_1,t15_aff_1), []). fof(t16_aff_1,axiom,( ! [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,u1_struct_0(A)) => ( r1_aff_1(A,B,B,C) & r1_aff_1(A,B,C,C) & r1_aff_1(A,B,C,B) ) ) ) ) ), file(aff_1,t16_aff_1), []). fof(t17_aff_2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v7_aff_2(A) => v8_aff_2(A) ) ) ), file(aff_2,t17_aff_2), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t21_aff_2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v11_aff_2(A) <=> v12_aff_2(A) ) ) ), file(aff_2,t21_aff_2), []). fof(t23_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r1_aff_1(A,B,D,E) & r2_analoaf(A,C,D,C,E) ) => ( r1_aff_1(A,B,C,D) | D = E ) ) ) ) ) ) ) ), file(aff_1,t23_aff_1), []). fof(t26_aff_2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) => v7_aff_2(A) ) ) ), file(aff_2,t26_aff_2), []). fof(t27_aff_2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v8_aff_2(A) => v12_aff_2(A) ) ) ), file(aff_2,t27_aff_2), []). fof(t2_conmetr1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v3_conmetr1(A) <=> ( v1_conmetr1(A) & v2_conmetr1(A) ) ) ) ), file(conmetr1,t2_conmetr1), []). fof(t33_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) <=> ? [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) & v1_aff_1(E,A) & r2_hidden(B,E) & r2_hidden(C,E) & r2_hidden(D,E) ) ) ) ) ) ) ), file(aff_1,t33_aff_1), []). fof(t39_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(E,A) & r2_hidden(B,E) & r2_hidden(C,E) & r1_aff_1(A,B,C,D) ) => ( B = C | r2_hidden(D,E) ) ) ) ) ) ) ) ), file(aff_1,t39_aff_1), []). fof(t3_subset,axiom,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), []). fof(t47_diraf,axiom,( ! [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,u1_struct_0(A)) => B = C ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ( r2_analoaf(A,B,C,C,B) & r2_analoaf(A,B,C,D,D) & ( ( r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,C,F,G) ) => ( B = C | r2_analoaf(A,D,E,F,G) ) ) & ( r2_analoaf(A,B,C,B,D) => r2_analoaf(A,C,B,C,D) ) ) ) ) ) ) ) ) & ~ ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => r2_analoaf(A,B,C,B,D) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & r2_analoaf(A,B,D,C,E) & C != E ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,D,C,E) ) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( r2_analoaf(A,D,B,B,E) & B != D & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r2_analoaf(A,C,B,B,F) & r2_analoaf(A,C,D,E,F) ) ) ) ) ) ) ) ) ) ), file(diraf,t47_diraf), []). 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(t53_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,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))) => ( ( r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,G) & r2_hidden(E,G) & r3_aff_1(A,F,G) ) => r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ) ), file(aff_1,t53_aff_1), []). fof(t55_aff_1,axiom,( ! [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_1(B,A) => r3_aff_1(A,B,B) ) ) ) ), file(aff_1,t55_aff_1), []). fof(t59_aff_1,axiom,( ! [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))) => ( ( r4_aff_1(A,C,D) & r2_hidden(B,C) & r2_hidden(B,D) ) => C = D ) ) ) ) ) ), file(aff_1,t59_aff_1), []). fof(t62_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(F,A) & r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,F) & r2_analoaf(A,B,C,D,E) ) => ( B = C | r2_hidden(E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t62_aff_1), []). fof(t65_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(F,A) & r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,F) & r2_hidden(E,F) ) => r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ), file(aff_1,t65_aff_1), []). fof(t66_aff_1,axiom,( ! [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,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(D,A) & r2_hidden(B,D) & r2_hidden(C,D) ) => r2_aff_1(A,B,C,D) ) ) ) ) ) ), file(aff_1,t66_aff_1), []). fof(t67_aff_1,axiom,( ! [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,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))) => ( ( r2_aff_1(A,B,C,D) & r2_aff_1(A,B,C,E) ) => ( B = C | r4_aff_1(A,D,E) ) ) ) ) ) ) ) ), file(aff_1,t67_aff_1), []). fof(t6_conmetr1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v11_aff_2(A) => v1_conmetr1(A) ) ) ), file(conmetr1,t6_conmetr1), []). fof(t74_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r2_analoaf(A,B,C,D,E) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r1_aff_1(A,B,C,F) & r1_aff_1(A,D,E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t74_aff_1), []). fof(t7_conmetr1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) => v2_conmetr1(A) ) ) ), file(conmetr1,t7_conmetr1), []).