% Mizar problem: t21_euclmetr,euclmetr,614,64 fof(t21_euclmetr,conjecture,( ! [A] : ( ( ~ v3_struct_0(A) & v3_analmetr(A) & l1_analmetr(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( ( r1_analmetr(B,C,D) & A = k2_analmetr(B,C,D) ) => v5_conaffm(A) ) ) ) ) ) ), inference(mizar_bg_added,[status(thm)],[abstractness_v1_analmetr,abstractness_v1_analoaf,antisymmetry_r2_hidden,cc10_membered,cc11_membered,cc12_membered,cc13_membered,cc14_membered,cc15_membered,cc16_membered,cc17_membered,cc18_membered,cc19_membered,cc1_analmetr,cc1_membered,cc20_membered,cc2_membered,cc3_membered,cc4_membered,cc6_membered,cc9_membered,commutativity_k2_xcmplx_0,commutativity_k3_real_1,commutativity_k3_xcmplx_0,commutativity_k4_real_1,commutativity_k4_rlvect_1,d11_analmetr,d11_rlvect_1,d1_analmetr,d1_geomtrap,d2_rlvect_1,d3_analmetr,d3_rlvect_1,d4_rlvect_1,d5_conaffm,d9_rlvect_1,dt_g1_analmetr,dt_g1_analoaf,dt_k1_analmetr,dt_k1_analoaf,dt_k1_diraf,dt_k1_domain_1,dt_k1_funct_1,dt_k1_numbers,dt_k1_real_1,dt_k1_rlvect_1,dt_k1_zfmisc_1,dt_k2_analmetr,dt_k2_real_1,dt_k2_rlvect_1,dt_k2_xcmplx_0,dt_k2_zfmisc_1,dt_k3_analmetr,dt_k3_real_1,dt_k3_rlvect_1,dt_k3_xcmplx_0,dt_k4_real_1,dt_k4_rlvect_1,dt_k4_tarski,dt_k4_xcmplx_0,dt_k5_numbers,dt_k5_ordinal2,dt_k5_rlvect_1,dt_k5_xcmplx_0,dt_k6_rlvect_1,dt_k8_funct_2,dt_l1_analmetr,dt_l1_analoaf,dt_l1_rlvect_1,dt_l1_struct_0,dt_l2_rlvect_1,dt_l2_struct_0,dt_m1_relset_1,dt_m1_subset_1,dt_m2_relset_1,dt_u1_analmetr,dt_u1_analoaf,dt_u1_rlvect_1,dt_u1_struct_0,dt_u2_rlvect_1,dt_u2_struct_0,existence_l1_analmetr,existence_l1_analoaf,existence_l1_rlvect_1,existence_l1_struct_0,existence_l2_rlvect_1,existence_l2_struct_0,existence_m1_relset_1,existence_m1_subset_1,existence_m2_relset_1,fc1_analmetr,fc2_analmetr,fc2_membered,fc3_analmetr,fc4_analmetr,fc5_membered,free_g1_analmetr,free_g1_analoaf,involutiveness_k1_real_1,involutiveness_k2_real_1,involutiveness_k4_xcmplx_0,involutiveness_k5_xcmplx_0,l28_euclmetr,l33_euclmetr,rc1_analmetr,rc1_membered,rc2_analmetr,rc3_analmetr,rc4_analmetr,redefinition_k1_domain_1,redefinition_k1_real_1,redefinition_k2_real_1,redefinition_k3_real_1,redefinition_k4_real_1,redefinition_k4_rlvect_1,redefinition_k5_numbers,redefinition_k8_funct_2,redefinition_m2_relset_1,reflexivity_r1_tarski,spc1_numerals,t12_analoaf,t15_aff_1,t16_aff_1,t16_euclmetr,t17_aff_1,t18_analmetr,t19_euclmetr,t1_arithm,t1_numerals,t1_subset,t23_rlvect_1,t24_rlvect_1,t28_analmetr,t2_arithm,t2_subset,t31_analmetr,t35_rlvect_1,t38_rlvect_1,t39_rlvect_1,t3_arithm,t3_subset,t47_analmetr,t48_rlvect_1,t4_geomtrap,t4_subset,t55_analmetr,t5_subset,t78_rlsub_2,t81_analmetr,t83_analmetr]), [file(euclmetr,t21_euclmetr)]). fof(abstractness_v1_analmetr,axiom,( ! [A] : ( l1_analmetr(A) => ( v1_analmetr(A) => A = g1_analmetr(u1_struct_0(A),u1_analoaf(A),u1_analmetr(A)) ) ) ), file(analmetr,v1_analmetr), []). fof(abstractness_v1_analoaf,axiom,( ! [A] : ( l1_analoaf(A) => ( v1_analoaf(A) => A = g1_analoaf(u1_struct_0(A),u1_analoaf(A)) ) ) ), file(analoaf,v1_analoaf), []). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(cc10_membered,axiom,( ! [A] : ( v1_membered(A) => ! [B] : ( m1_subset_1(B,A) => v1_xcmplx_0(B) ) ) ), file(membered,cc10_membered), []). fof(cc11_membered,axiom,( ! [A] : ( v2_membered(A) => ! [B] : ( m1_subset_1(B,A) => ( v1_xcmplx_0(B) & v1_xreal_0(B) ) ) ) ), file(membered,cc11_membered), []). fof(cc12_membered,axiom,( ! [A] : ( v3_membered(A) => ! [B] : ( m1_subset_1(B,A) => ( v1_xcmplx_0(B) & v1_xreal_0(B) & v1_rat_1(B) ) ) ) ), file(membered,cc12_membered), []). fof(cc13_membered,axiom,( ! [A] : ( v4_membered(A) => ! [B] : ( m1_subset_1(B,A) => ( v1_xcmplx_0(B) & v1_xreal_0(B) & v1_int_1(B) & v1_rat_1(B) ) ) ) ), file(membered,cc13_membered), []). fof(cc14_membered,axiom,( ! [A] : ( v5_membered(A) => ! [B] : ( m1_subset_1(B,A) => ( v1_xcmplx_0(B) & v4_ordinal2(B) & v1_xreal_0(B) & v1_int_1(B) & v1_rat_1(B) ) ) ) ), file(membered,cc14_membered), []). fof(cc15_membered,axiom,( ! [A] : ( v1_xboole_0(A) => ( v1_membered(A) & v2_membered(A) & v3_membered(A) & v4_membered(A) & v5_membered(A) ) ) ), file(membered,cc15_membered), []). fof(cc16_membered,axiom,( ! [A] : ( v1_membered(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => v1_membered(B) ) ) ), file(membered,cc16_membered), []). fof(cc17_membered,axiom,( ! [A] : ( v2_membered(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ( v1_membered(B) & v2_membered(B) ) ) ) ), file(membered,cc17_membered), []). fof(cc18_membered,axiom,( ! [A] : ( v3_membered(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ( v1_membered(B) & v2_membered(B) & v3_membered(B) ) ) ) ), file(membered,cc18_membered), []). fof(cc19_membered,axiom,( ! [A] : ( v4_membered(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ( v1_membered(B) & v2_membered(B) & v3_membered(B) & v4_membered(B) ) ) ) ), file(membered,cc19_membered), []). fof(cc1_analmetr,axiom,( ! [A] : ( l1_analmetr(A) => ( ( ~ v3_struct_0(A) & v3_analmetr(A) ) => ( ~ v3_struct_0(A) & v2_analmetr(A) ) ) ) ), file(analmetr,cc1_analmetr), []). fof(cc1_membered,axiom,( ! [A] : ( v5_membered(A) => v4_membered(A) ) ), file(membered,cc1_membered), []). fof(cc20_membered,axiom,( ! [A] : ( v5_membered(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ( v1_membered(B) & v2_membered(B) & v3_membered(B) & v4_membered(B) & v5_membered(B) ) ) ) ), file(membered,cc20_membered), []). fof(cc2_membered,axiom,( ! [A] : ( v4_membered(A) => v3_membered(A) ) ), file(membered,cc2_membered), []). fof(cc3_membered,axiom,( ! [A] : ( v3_membered(A) => v2_membered(A) ) ), file(membered,cc3_membered), []). fof(cc4_membered,axiom,( ! [A] : ( v2_membered(A) => v1_membered(A) ) ), file(membered,cc4_membered), []). fof(cc6_membered,axiom,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(k1_numbers)) => ( v1_membered(A) & v2_membered(A) ) ) ), file(membered,cc6_membered), []). fof(cc9_membered,axiom,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(k5_numbers)) => ( v1_membered(A) & v2_membered(A) & v3_membered(A) & v4_membered(A) & v5_membered(A) ) ) ), file(membered,cc9_membered), []). fof(commutativity_k2_xcmplx_0,axiom,( ! [A,B] : ( ( v1_xcmplx_0(A) & v1_xcmplx_0(B) ) => k2_xcmplx_0(A,B) = k2_xcmplx_0(B,A) ) ), file(xcmplx_0,k2_xcmplx_0), []). fof(commutativity_k3_real_1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k1_numbers) & m1_subset_1(B,k1_numbers) ) => k3_real_1(A,B) = k3_real_1(B,A) ) ), file(real_1,k3_real_1), []). fof(commutativity_k3_xcmplx_0,axiom,( ! [A,B] : ( ( v1_xcmplx_0(A) & v1_xcmplx_0(B) ) => k3_xcmplx_0(A,B) = k3_xcmplx_0(B,A) ) ), file(xcmplx_0,k3_xcmplx_0), []). fof(commutativity_k4_real_1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k1_numbers) & m1_subset_1(B,k1_numbers) ) => k4_real_1(A,B) = k4_real_1(B,A) ) ), file(real_1,k4_real_1), []). fof(commutativity_k4_rlvect_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & l1_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => k4_rlvect_1(A,B,C) = k4_rlvect_1(A,C,B) ) ), file(rlvect_1,k4_rlvect_1), []). fof(d11_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analmetr(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)) => ( r6_analmetr(A,B,C,D) <=> r4_analmetr(A,B,C,B,D) ) ) ) ) ) ), file(analmetr,d11_analmetr), []). fof(d11_rlvect_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k6_rlvect_1(A,B,C) = k2_rlvect_1(A,B,k5_rlvect_1(A,C)) ) ) ) ), file(rlvect_1,d11_rlvect_1), []). fof(d1_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) <=> ( ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ? [E] : ( m1_subset_1(E,k1_numbers) & ? [F] : ( m1_subset_1(F,k1_numbers) & D = k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,F)) ) ) ) & ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,E)) = k1_rlvect_1(A) => ( D = 0 & E = 0 ) ) ) ) ) ) ) ) ) ), file(analmetr,d1_analmetr), []). fof(d1_geomtrap,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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_geomtrap(A,B,C,D,E) <=> ( r1_analoaf(A,B,C,D,E) | r1_analoaf(A,B,C,E,D) ) ) ) ) ) ) ) ), file(geomtrap,d1_geomtrap), []). fof(d2_rlvect_1,axiom,( ! [A] : ( l2_struct_0(A) => k1_rlvect_1(A) = u2_struct_0(A) ) ), file(rlvect_1,d2_rlvect_1), []). fof(d3_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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)) => ( r3_analmetr(A,B,C,D,E,F,G) <=> r2_analmetr(A,k6_rlvect_1(A,C,B),k6_rlvect_1(A,E,D),F,G) ) ) ) ) ) ) ) ) ), file(analmetr,d3_analmetr), []). fof(d3_rlvect_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k2_rlvect_1(A,B,C) = k8_funct_2(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A),u1_rlvect_1(A),k1_domain_1(u1_struct_0(A),u1_struct_0(A),B,C)) ) ) ) ), file(rlvect_1,d3_rlvect_1), []). fof(d4_rlvect_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_numbers) => k3_rlvect_1(A,B,C) = k8_funct_2(k2_zfmisc_1(k1_numbers,u1_struct_0(A)),u1_struct_0(A),u2_rlvect_1(A),k1_domain_1(k1_numbers,u1_struct_0(A),C,B)) ) ) ) ), file(rlvect_1,d4_rlvect_1), []). fof(d5_conaffm,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_analmetr(A) & l1_analmetr(A) ) => ( v5_conaffm(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)) => ( ( r5_analmetr(A,B,G,B,H) & r5_analmetr(A,B,C,B,D) & r5_analmetr(A,B,E,B,F) & r6_analmetr(A,B,C,E) & r6_analmetr(A,B,D,F) & r5_analmetr(A,C,G,D,H) & r5_analmetr(A,E,G,F,H) ) => ( B = C | B = D | B = E | B = F | B = G | B = H | C = E | r6_analmetr(A,B,G,C) | r4_analmetr(A,C,D,E,F) ) ) ) ) ) ) ) ) ) ) ) ), file(conaffm,d5_conaffm), []). fof(d9_rlvect_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ( v7_rlvect_1(A) <=> ( ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k3_real_1(B,C)) = k2_rlvect_1(A,k3_rlvect_1(A,D,B),k3_rlvect_1(A,D,C)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k4_real_1(B,C)) = k3_rlvect_1(A,k3_rlvect_1(A,D,C),B) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_rlvect_1(A,B,1) = B ) ) ) ) ), file(rlvect_1,d9_rlvect_1), []). fof(dt_g1_analmetr,axiom,( ! [A,B,C] : ( ( m1_relset_1(B,k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) & m1_relset_1(C,k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) ) => ( v1_analmetr(g1_analmetr(A,B,C)) & l1_analmetr(g1_analmetr(A,B,C)) ) ) ), file(analmetr,g1_analmetr), []). fof(dt_g1_analoaf,axiom,( ! [A,B] : ( m1_relset_1(B,k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) => ( v1_analoaf(g1_analoaf(A,B)) & l1_analoaf(g1_analoaf(A,B)) ) ) ), file(analoaf,g1_analoaf), []). fof(dt_k1_analmetr,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m2_relset_1(k1_analmetr(A,B,C),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) ) ), file(analmetr,k1_analmetr), []). fof(dt_k1_analoaf,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => m2_relset_1(k1_analoaf(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) ) ), file(analoaf,k1_analoaf), []). fof(dt_k1_diraf,axiom,( ! [A,B] : ( ( ~ v1_xboole_0(A) & m1_relset_1(B,k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) ) => m2_relset_1(k1_diraf(A,B),k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) ) ), file(diraf,k1_diraf), []). fof(dt_k1_domain_1,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & m1_subset_1(C,A) & m1_subset_1(D,B) ) => m1_subset_1(k1_domain_1(A,B,C,D),k2_zfmisc_1(A,B)) ) ), file(domain_1,k1_domain_1), []). fof(dt_k1_funct_1,axiom,( $true ), file(funct_1,k1_funct_1), []). fof(dt_k1_numbers,axiom,( $true ), file(numbers,k1_numbers), []). fof(dt_k1_real_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => m1_subset_1(k1_real_1(A),k1_numbers) ) ), file(real_1,k1_real_1), []). fof(dt_k1_rlvect_1,axiom,( ! [A] : ( l2_struct_0(A) => m1_subset_1(k1_rlvect_1(A),u1_struct_0(A)) ) ), file(rlvect_1,k1_rlvect_1), []). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), []). fof(dt_k2_analmetr,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => ( v1_analmetr(k2_analmetr(A,B,C)) & l1_analmetr(k2_analmetr(A,B,C)) ) ) ), file(analmetr,k2_analmetr), []). fof(dt_k2_real_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => m1_subset_1(k2_real_1(A),k1_numbers) ) ), file(real_1,k2_real_1), []). fof(dt_k2_rlvect_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m1_subset_1(k2_rlvect_1(A,B,C),u1_struct_0(A)) ) ), file(rlvect_1,k2_rlvect_1), []). fof(dt_k2_xcmplx_0,axiom,( $true ), file(xcmplx_0,k2_xcmplx_0), []). fof(dt_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), []). fof(dt_k3_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analmetr(A) ) => ( v1_analoaf(k3_analmetr(A)) & l1_analoaf(k3_analmetr(A)) ) ) ), file(analmetr,k3_analmetr), []). fof(dt_k3_real_1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k1_numbers) & m1_subset_1(B,k1_numbers) ) => m1_subset_1(k3_real_1(A,B),k1_numbers) ) ), file(real_1,k3_real_1), []). fof(dt_k3_rlvect_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,k1_numbers) ) => m1_subset_1(k3_rlvect_1(A,B,C),u1_struct_0(A)) ) ), file(rlvect_1,k3_rlvect_1), []). fof(dt_k3_xcmplx_0,axiom,( $true ), file(xcmplx_0,k3_xcmplx_0), []). fof(dt_k4_real_1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k1_numbers) & m1_subset_1(B,k1_numbers) ) => m1_subset_1(k4_real_1(A,B),k1_numbers) ) ), file(real_1,k4_real_1), []). fof(dt_k4_rlvect_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & l1_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m1_subset_1(k4_rlvect_1(A,B,C),u1_struct_0(A)) ) ), file(rlvect_1,k4_rlvect_1), []). fof(dt_k4_tarski,axiom,( $true ), file(tarski,k4_tarski), []). fof(dt_k4_xcmplx_0,axiom,( ! [A] : ( v1_xcmplx_0(A) => v1_xcmplx_0(k4_xcmplx_0(A)) ) ), file(xcmplx_0,k4_xcmplx_0), []). fof(dt_k5_numbers,axiom,( m1_subset_1(k5_numbers,k1_zfmisc_1(k1_numbers)) ), file(numbers,k5_numbers), []). fof(dt_k5_ordinal2,axiom,( $true ), file(ordinal2,k5_ordinal2), []). fof(dt_k5_rlvect_1,axiom,( ! [A,B] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) ) => m1_subset_1(k5_rlvect_1(A,B),u1_struct_0(A)) ) ), file(rlvect_1,k5_rlvect_1), []). fof(dt_k5_xcmplx_0,axiom,( ! [A] : ( v1_xcmplx_0(A) => v1_xcmplx_0(k5_xcmplx_0(A)) ) ), file(xcmplx_0,k5_xcmplx_0), []). fof(dt_k6_rlvect_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m1_subset_1(k6_rlvect_1(A,B,C),u1_struct_0(A)) ) ), file(rlvect_1,k6_rlvect_1), []). fof(dt_k8_funct_2,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & v1_funct_1(C) & v1_funct_2(C,A,B) & m1_relset_1(C,A,B) & m1_subset_1(D,A) ) => m1_subset_1(k8_funct_2(A,B,C,D),B) ) ), file(funct_2,k8_funct_2), []). fof(dt_l1_analmetr,axiom,( ! [A] : ( l1_analmetr(A) => l1_analoaf(A) ) ), file(analmetr,l1_analmetr), []). fof(dt_l1_analoaf,axiom,( ! [A] : ( l1_analoaf(A) => l1_struct_0(A) ) ), file(analoaf,l1_analoaf), []). fof(dt_l1_rlvect_1,axiom,( ! [A] : ( l1_rlvect_1(A) => l2_struct_0(A) ) ), file(rlvect_1,l1_rlvect_1), []). fof(dt_l1_struct_0,axiom,( $true ), file(struct_0,l1_struct_0), []). fof(dt_l2_rlvect_1,axiom,( ! [A] : ( l2_rlvect_1(A) => l1_rlvect_1(A) ) ), file(rlvect_1,l2_rlvect_1), []). fof(dt_l2_struct_0,axiom,( ! [A] : ( l2_struct_0(A) => l1_struct_0(A) ) ), file(struct_0,l2_struct_0), []). 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_analmetr,axiom,( ! [A] : ( l1_analmetr(A) => m2_relset_1(u1_analmetr(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) ) ), file(analmetr,u1_analmetr), []). fof(dt_u1_analoaf,axiom,( ! [A] : ( l1_analoaf(A) => m2_relset_1(u1_analoaf(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) ) ), file(analoaf,u1_analoaf), []). fof(dt_u1_rlvect_1,axiom,( ! [A] : ( l1_rlvect_1(A) => ( v1_funct_1(u1_rlvect_1(A)) & v1_funct_2(u1_rlvect_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) & m2_relset_1(u1_rlvect_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ), file(rlvect_1,u1_rlvect_1), []). fof(dt_u1_struct_0,axiom,( $true ), file(struct_0,u1_struct_0), []). fof(dt_u2_rlvect_1,axiom,( ! [A] : ( l2_rlvect_1(A) => ( v1_funct_1(u2_rlvect_1(A)) & v1_funct_2(u2_rlvect_1(A),k2_zfmisc_1(k1_numbers,u1_struct_0(A)),u1_struct_0(A)) & m2_relset_1(u2_rlvect_1(A),k2_zfmisc_1(k1_numbers,u1_struct_0(A)),u1_struct_0(A)) ) ) ), file(rlvect_1,u2_rlvect_1), []). fof(dt_u2_struct_0,axiom,( ! [A] : ( l2_struct_0(A) => m1_subset_1(u2_struct_0(A),u1_struct_0(A)) ) ), file(struct_0,u2_struct_0), []). fof(existence_l1_analmetr,axiom,( ? [A] : l1_analmetr(A) ), file(analmetr,l1_analmetr), []). fof(existence_l1_analoaf,axiom,( ? [A] : l1_analoaf(A) ), file(analoaf,l1_analoaf), []). fof(existence_l1_rlvect_1,axiom,( ? [A] : l1_rlvect_1(A) ), file(rlvect_1,l1_rlvect_1), []). fof(existence_l1_struct_0,axiom,( ? [A] : l1_struct_0(A) ), file(struct_0,l1_struct_0), []). fof(existence_l2_rlvect_1,axiom,( ? [A] : l2_rlvect_1(A) ), file(rlvect_1,l2_rlvect_1), []). fof(existence_l2_struct_0,axiom,( ? [A] : l2_struct_0(A) ), file(struct_0,l2_struct_0), []). 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_analmetr,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => ( ~ v3_struct_0(k2_analmetr(A,B,C)) & v1_analmetr(k2_analmetr(A,B,C)) ) ) ), file(analmetr,fc1_analmetr), []). fof(fc2_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analmetr(A) ) => ( ~ v3_struct_0(k3_analmetr(A)) & v1_analoaf(k3_analmetr(A)) ) ) ), file(analmetr,fc2_analmetr), []). fof(fc2_membered,axiom, ( ~ v1_xboole_0(k1_numbers) & v1_membered(k1_numbers) & v2_membered(k1_numbers) ), file(membered,fc2_membered), []). fof(fc3_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v2_analmetr(A) & l1_analmetr(A) ) => ( ~ v3_struct_0(k3_analmetr(A)) & ~ v3_realset2(k3_analmetr(A)) & v1_analoaf(k3_analmetr(A)) & v1_diraf(k3_analmetr(A)) ) ) ), file(analmetr,fc3_analmetr), []). fof(fc4_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_analmetr(A) & l1_analmetr(A) ) => ( ~ v3_struct_0(k3_analmetr(A)) & ~ v3_realset2(k3_analmetr(A)) & v1_analoaf(k3_analmetr(A)) & v1_diraf(k3_analmetr(A)) & v2_diraf(k3_analmetr(A)) ) ) ), file(analmetr,fc4_analmetr), []). fof(fc5_membered,axiom, ( v1_membered(k5_ordinal2) & v2_membered(k5_ordinal2) & v3_membered(k5_ordinal2) & v4_membered(k5_ordinal2) & v5_membered(k5_ordinal2) ), file(membered,fc5_membered), []). fof(free_g1_analmetr,axiom,( ! [A,B,C] : ( ( m1_relset_1(B,k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) & m1_relset_1(C,k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) ) => ! [D,E,F] : ( g1_analmetr(A,B,C) = g1_analmetr(D,E,F) => ( A = D & B = E & C = F ) ) ) ), file(analmetr,g1_analmetr), []). fof(free_g1_analoaf,axiom,( ! [A,B] : ( m1_relset_1(B,k2_zfmisc_1(A,A),k2_zfmisc_1(A,A)) => ! [C,D] : ( g1_analoaf(A,B) = g1_analoaf(C,D) => ( A = C & B = D ) ) ) ), file(analoaf,g1_analoaf), []). fof(involutiveness_k1_real_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => k1_real_1(k1_real_1(A)) = A ) ), file(real_1,k1_real_1), []). fof(involutiveness_k2_real_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => k2_real_1(k2_real_1(A)) = A ) ), file(real_1,k2_real_1), []). fof(involutiveness_k4_xcmplx_0,axiom,( ! [A] : ( v1_xcmplx_0(A) => k4_xcmplx_0(k4_xcmplx_0(A)) = A ) ), file(xcmplx_0,k4_xcmplx_0), []). fof(involutiveness_k5_xcmplx_0,axiom,( ! [A] : ( v1_xcmplx_0(A) => k5_xcmplx_0(k5_xcmplx_0(A)) = A ) ), file(xcmplx_0,k5_xcmplx_0), []). fof(l28_euclmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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)) => ( k6_rlvect_1(A,k6_rlvect_1(A,B,D),k6_rlvect_1(A,C,D)) = k6_rlvect_1(A,B,C) & k6_rlvect_1(A,k4_rlvect_1(A,B,D),k4_rlvect_1(A,C,D)) = k6_rlvect_1(A,B,C) ) ) ) ) ) ), file(euclmetr,l28_euclmetr), []). fof(l33_euclmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_analmetr(A,B,C) => ! [D] : ( m1_subset_1(D,k1_numbers) => ! [E] : ( m1_subset_1(E,k1_numbers) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ( k4_rlvect_1(A,k3_rlvect_1(A,B,D),k3_rlvect_1(A,C,F)) = k4_rlvect_1(A,k3_rlvect_1(A,B,E),k3_rlvect_1(A,C,G)) => ( D = E & F = G ) ) ) ) ) ) ) ) ) ) ), file(euclmetr,l33_euclmetr), []). fof(rc1_analmetr,axiom,( ? [A] : ( l1_analmetr(A) & v1_analmetr(A) ) ), file(analmetr,rc1_analmetr), []). fof(rc1_membered,axiom,( ? [A] : ( ~ v1_xboole_0(A) & v1_membered(A) & v2_membered(A) & v3_membered(A) & v4_membered(A) & v5_membered(A) ) ), file(membered,rc1_membered), []). fof(rc2_analmetr,axiom,( ? [A] : ( l1_analmetr(A) & ~ v3_struct_0(A) ) ), file(analmetr,rc2_analmetr), []). fof(rc3_analmetr,axiom,( ? [A] : ( l1_analmetr(A) & ~ v3_struct_0(A) & v1_analmetr(A) & v2_analmetr(A) ) ), file(analmetr,rc3_analmetr), []). fof(rc4_analmetr,axiom,( ? [A] : ( l1_analmetr(A) & ~ v3_struct_0(A) & v1_analmetr(A) & v3_analmetr(A) ) ), file(analmetr,rc4_analmetr), []). fof(redefinition_k1_domain_1,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & m1_subset_1(C,A) & m1_subset_1(D,B) ) => k1_domain_1(A,B,C,D) = k4_tarski(C,D) ) ), file(domain_1,k1_domain_1), []). fof(redefinition_k1_real_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => k1_real_1(A) = k4_xcmplx_0(A) ) ), file(real_1,k1_real_1), []). fof(redefinition_k2_real_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => k2_real_1(A) = k5_xcmplx_0(A) ) ), file(real_1,k2_real_1), []). fof(redefinition_k3_real_1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k1_numbers) & m1_subset_1(B,k1_numbers) ) => k3_real_1(A,B) = k2_xcmplx_0(A,B) ) ), file(real_1,k3_real_1), []). fof(redefinition_k4_real_1,axiom,( ! [A,B] : ( ( m1_subset_1(A,k1_numbers) & m1_subset_1(B,k1_numbers) ) => k4_real_1(A,B) = k3_xcmplx_0(A,B) ) ), file(real_1,k4_real_1), []). fof(redefinition_k4_rlvect_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & l1_rlvect_1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => k4_rlvect_1(A,B,C) = k2_rlvect_1(A,B,C) ) ), file(rlvect_1,k4_rlvect_1), []). fof(redefinition_k5_numbers,axiom,( k5_numbers = k5_ordinal2 ), file(numbers,k5_numbers), []). fof(redefinition_k8_funct_2,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & v1_funct_1(C) & v1_funct_2(C,A,B) & m1_relset_1(C,A,B) & m1_subset_1(D,A) ) => k8_funct_2(A,B,C,D) = k1_funct_1(C,D) ) ), file(funct_2,k8_funct_2), []). 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(spc1_numerals,axiom, ( v2_xreal_0(1) & m1_subset_1(1,k5_numbers) ), file(numerals,spc1_numerals), []). fof(t12_analoaf,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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_numbers) => ( k3_rlvect_1(A,B,D) = C => ( D = 0 | B = k3_rlvect_1(A,C,k2_real_1(D)) ) ) ) ) ) ) ), file(analoaf,t12_analoaf), []). 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(t16_euclmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_analmetr(A) & l1_analmetr(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)) => ( ( r5_analmetr(A,B,C,B,D) & r5_analmetr(A,B,E,B,F) & r5_analmetr(A,B,E,B,G) & r5_analmetr(A,C,E,D,F) & r5_analmetr(A,C,E,D,G) ) => ( r6_analmetr(A,B,C,E) | B = D | F = G ) ) ) ) ) ) ) ) ) ), file(euclmetr,t16_euclmetr), []). fof(t17_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)) => ( ( r1_aff_1(A,B,C,D) & r1_aff_1(A,B,C,E) & r1_aff_1(A,B,C,F) ) => ( B = C | r1_aff_1(A,D,E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t17_aff_1), []). fof(t18_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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_analoaf(A,B,C,D,E) | r1_analoaf(A,B,C,E,D) ) & ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ~ ( k3_rlvect_1(A,k6_rlvect_1(A,C,B),F) = k3_rlvect_1(A,k6_rlvect_1(A,E,D),G) & ~ ( F = 0 & G = 0 ) ) ) ) ) & ~ ( ? [F] : ( m1_subset_1(F,k1_numbers) & ? [G] : ( m1_subset_1(G,k1_numbers) & k3_rlvect_1(A,k6_rlvect_1(A,C,B),F) = k3_rlvect_1(A,k6_rlvect_1(A,E,D),G) & ~ ( F = 0 & G = 0 ) ) ) & ~ r1_analoaf(A,B,C,D,E) & ~ r1_analoaf(A,B,C,E,D) ) ) ) ) ) ) ) ), file(analmetr,t18_analmetr), []). fof(t19_euclmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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_analmetr(A,B,C) & k1_rlvect_1(A) != D & k1_rlvect_1(A) != E & r2_analmetr(A,D,E,B,C) & ! [F] : ( m1_subset_1(F,k1_numbers) => ~ ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ( r2_analmetr(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),k4_rlvect_1(A,k3_rlvect_1(A,B,k4_real_1(F,H)),k3_rlvect_1(A,C,k1_real_1(k4_real_1(F,G)))),B,C) & r2_analmetr(A,k6_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,G),k3_rlvect_1(A,C,H)),D),k6_rlvect_1(A,k4_rlvect_1(A,k3_rlvect_1(A,B,k4_real_1(F,H)),k3_rlvect_1(A,C,k1_real_1(k4_real_1(F,G)))),E),B,C) ) ) ) ) ) ) ) ) ) ) ), file(euclmetr,t19_euclmetr), []). fof(t1_arithm,axiom,( ! [A] : ( v1_xcmplx_0(A) => k2_xcmplx_0(A,0) = A ) ), file(arithm,t1_arithm), []). fof(t1_numerals,axiom,( m1_subset_1(0,k5_numbers) ), file(numerals,t1_numerals), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t23_rlvect_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ( ( A = 0 | C = k1_rlvect_1(B) ) => k3_rlvect_1(B,C,A) = k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t23_rlvect_1), []). fof(t24_rlvect_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ~ ( k3_rlvect_1(B,C,A) = k1_rlvect_1(B) & A != 0 & C != k1_rlvect_1(B) ) ) ) ) ), file(rlvect_1,t24_rlvect_1), []). fof(t28_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( u1_struct_0(k2_analmetr(A,B,C)) = u1_struct_0(A) & u1_analoaf(k2_analmetr(A,B,C)) = k1_diraf(u1_struct_0(A),k1_analoaf(A)) & u1_analmetr(k2_analmetr(A,B,C)) = k1_analmetr(A,B,C) ) ) ) ) ), file(analmetr,t28_analmetr), []). fof(t2_arithm,axiom,( ! [A] : ( v1_xcmplx_0(A) => k3_xcmplx_0(A,0) = 0 ) ), file(arithm,t2_arithm), []). fof(t2_subset,axiom,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), []). fof(t31_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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(k2_analmetr(A,F,G))) => ! [I] : ( m1_subset_1(I,u1_struct_0(k2_analmetr(A,F,G))) => ! [J] : ( m1_subset_1(J,u1_struct_0(k2_analmetr(A,F,G))) => ! [K] : ( m1_subset_1(K,u1_struct_0(k2_analmetr(A,F,G))) => ( ( H = B & I = C & J = D & K = E ) => ( r5_analmetr(k2_analmetr(A,F,G),H,J,I,K) <=> r3_analmetr(A,B,D,C,E,F,G) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(analmetr,t31_analmetr), []). fof(t35_rlvect_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A) => B = C ) ) ) ) ), file(rlvect_1,t35_rlvect_1), []). fof(t38_rlvect_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k3_rlvect_1(B,C,k1_real_1(A)) ) ) ) ), file(rlvect_1,t38_rlvect_1), []). fof(t39_rlvect_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_rlvect_1(B,k5_rlvect_1(B,C),A) = k5_rlvect_1(B,k3_rlvect_1(B,C,A)) ) ) ) ), file(rlvect_1,t39_rlvect_1), []). fof(t3_arithm,axiom,( ! [A] : ( v1_xcmplx_0(A) => k3_xcmplx_0(1,A) = A ) ), file(arithm,t3_arithm), []). fof(t3_subset,axiom,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), []). fof(t47_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_analmetr(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) <=> m1_subset_1(B,u1_struct_0(k3_analmetr(A))) ) ) ), file(analmetr,t47_analmetr), []). fof(t48_rlvect_1,axiom,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k3_rlvect_1(B,k6_rlvect_1(B,C,D),A) = k6_rlvect_1(B,k3_rlvect_1(B,C,A),k3_rlvect_1(B,D,A)) ) ) ) ) ), file(rlvect_1,t48_rlvect_1), []). fof(t4_geomtrap,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & l2_rlvect_1(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(k2_analmetr(A,B,C))) => ! [I] : ( m1_subset_1(I,u1_struct_0(k2_analmetr(A,B,C))) => ! [J] : ( m1_subset_1(J,u1_struct_0(k2_analmetr(A,B,C))) => ! [K] : ( m1_subset_1(K,u1_struct_0(k2_analmetr(A,B,C))) => ( ( H = D & I = E & J = F & K = G ) => ( r4_analmetr(k2_analmetr(A,B,C),H,I,J,K) <=> r1_geomtrap(A,D,E,F,G) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(geomtrap,t4_geomtrap), []). 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(t55_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v2_analmetr(A) & l1_analmetr(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(k3_analmetr(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k3_analmetr(A))) => ! [G] : ( m1_subset_1(G,u1_struct_0(k3_analmetr(A))) => ( ( B = E & C = F & D = G ) => ( r6_analmetr(A,B,C,D) <=> r1_aff_1(k3_analmetr(A),E,F,G) ) ) ) ) ) ) ) ) ) ), file(analmetr,t55_analmetr), []). 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(t78_rlsub_2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(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)) => ( B = k2_rlvect_1(A,C,D) <=> C = k6_rlvect_1(A,B,D) ) ) ) ) ) ), file(rlsub_2,t78_rlsub_2), []). fof(t81_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v2_analmetr(A) & l1_analmetr(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)) => ( r4_analmetr(A,B,C,D,E) => ( r4_analmetr(A,B,C,E,D) & r4_analmetr(A,C,B,D,E) & r4_analmetr(A,C,B,E,D) & r4_analmetr(A,D,E,B,C) & r4_analmetr(A,D,E,C,B) & r4_analmetr(A,E,D,B,C) & r4_analmetr(A,E,D,C,B) ) ) ) ) ) ) ) ), file(analmetr,t81_analmetr), []). fof(t83_analmetr,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v2_analmetr(A) & l1_analmetr(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)) => ( r5_analmetr(A,B,C,D,E) => ( r5_analmetr(A,B,C,E,D) & r5_analmetr(A,C,B,D,E) & r5_analmetr(A,C,B,E,D) & r5_analmetr(A,D,E,B,C) & r5_analmetr(A,D,E,C,B) & r5_analmetr(A,E,D,B,C) & r5_analmetr(A,E,D,C,B) ) ) ) ) ) ) ) ), file(analmetr,t83_analmetr), []).