fof(t14_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v3_xreal_0(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(k2_brouwer(2,B,A)),u1_struct_0(k2_brouwer(2,B,A))) & v5_pre_topc(C,k2_brouwer(2,B,A),k2_brouwer(2,B,A)) & m2_relset_1(C,u1_struct_0(k2_brouwer(2,B,A)),u1_struct_0(k2_brouwer(2,B,A))) ) => r3_abian(C) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_toprealb,t3_brouwer,t17_topreal9,t4_tsep_1,t10_brouwer,t13_brouwer,d19_borsuk_1,d5_abian,t11_brouwer,d20_borsuk_1,t2_brouwer,d5_abian,d1_funct_2,d1_tarski,d3_abian,d5_funct_1,d1_tarski]), [file(brouwer,t14_brouwer),interesting(1.00)]). fof(t13_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & v2_xreal_0(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(k2_brouwer(2,B,A)),u1_struct_0(k2_brouwer(2,B,A))) & v5_pre_topc(C,k2_brouwer(2,B,A),k2_brouwer(2,B,A)) & m2_relset_1(C,u1_struct_0(k2_brouwer(2,B,A)),u1_struct_0(k2_brouwer(2,B,A))) ) => ( ~ r3_abian(C) => v5_pre_topc(k5_brouwer(2,A,B,C),k2_brouwer(2,B,A),k7_toprealb(2,B,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_borsuk_3,t1_tsep_1,t27_xboole_1,t9_toprealb,t3_brouwer,t17_topreal9,t3_brouwer,t2_topmetr,t46_euclid,t24_toprns_1,t8_topreal9,t106_zfmisc_1,d5_borsuk_1,t19_topreal9,t7_topreal9,t3_xboole_0,d3_xboole_0,t12_pre_topc,t12_pre_topc,t50_borsuk_1,s1_pscomp_1,t50_borsuk_1,s1_pscomp_1,t50_borsuk_1,s1_pscomp_1,t50_borsuk_1,s1_pscomp_1,t50_borsuk_1,s1_pscomp_1,t50_borsuk_1,s1_pscomp_1,t24_topmetr,t24_topmetr,t62_borsuk_5,t40_rcomp_1,d1_xreal_0,d3_tarski,t57_euclid,t8_xreal_1,t92_real_1,l1_brouwer,d2_zfmisc_1,t66_pscomp_1,t46_borsuk_1,d3_tarski,t116_funct_2,t106_zfmisc_1,t56_euclid,t11_xreal_1,t47_rcomp_1,t20_jgraph_2,t83_topreal6,t24_topmetr,t62_borsuk_5,t40_rcomp_1,d1_xreal_0,d3_tarski,t57_euclid,t8_xreal_1,t92_real_1,l1_brouwer,d2_zfmisc_1,t68_pscomp_1,t46_borsuk_1,d3_tarski,t116_funct_2,t106_zfmisc_1,t56_euclid,t11_xreal_1,t47_rcomp_1,t20_jgraph_2,t83_topreal6,t24_topmetr,t62_borsuk_5,t40_rcomp_1,d1_xreal_0,d3_tarski,d3_tarski,t57_euclid,t73_real_1,t8_xreal_1,t92_real_1,t57_euclid,t8_xreal_1,t92_real_1,d2_zfmisc_1,t66_pscomp_1,t46_borsuk_1,d3_tarski,t116_funct_2,t106_zfmisc_1,t56_euclid,t8_xreal_1,t92_real_1,t11_xreal_1,t9_seq_2,t106_zfmisc_1,t56_euclid,t8_xreal_1,t92_real_1,t11_xreal_1,t9_seq_2,t10_xreal_1,t143_complex1,t138_complex1,t2_xreal_1,t8_rcomp_1,t20_jgraph_2,t83_topreal6,t24_topmetr,t62_borsuk_5,t40_rcomp_1,d1_xreal_0,d3_tarski,d3_tarski,t57_euclid,t73_real_1,t8_xreal_1,t92_real_1,t57_euclid,t8_xreal_1,t92_real_1,d2_zfmisc_1,t68_pscomp_1,t46_borsuk_1,d3_tarski,t116_funct_2,t106_zfmisc_1,t56_euclid,t8_xreal_1,t92_real_1,t11_xreal_1,t9_seq_2,t106_zfmisc_1,t56_euclid,t8_xreal_1,t92_real_1,t11_xreal_1,t9_seq_2,t10_xreal_1,t143_complex1,t138_complex1,t2_xreal_1,t8_rcomp_1,t20_jgraph_2,t83_topreal6,t24_topmetr,t62_borsuk_5,t40_rcomp_1,d1_xreal_0,d3_tarski,t57_euclid,t8_xreal_1,t92_real_1,l1_brouwer,d2_zfmisc_1,t66_pscomp_1,t46_borsuk_1,d3_tarski,t116_funct_2,t106_zfmisc_1,t56_euclid,t8_xreal_1,t92_real_1,t11_xreal_1,t9_seq_2,t138_complex1,t8_rcomp_1,t20_jgraph_2,t83_topreal6,t24_topmetr,t62_borsuk_5,t40_rcomp_1,d1_xreal_0,d3_tarski,t57_euclid,t8_xreal_1,t92_real_1,l1_brouwer,d2_zfmisc_1,t68_pscomp_1,t46_borsuk_1,d3_tarski,t116_funct_2,t106_zfmisc_1,t56_euclid,t8_xreal_1,t92_real_1,t11_xreal_1,t9_seq_2,t138_complex1,t8_rcomp_1,t20_jgraph_2,t83_topreal6,d1_xreal_0,l19_brouwer,t1_jordan1,t12_pre_topc,d1_funct_2,d1_funct_2,d1_funct_2,t2_topmetr,d3_xboole_0,t72_funct_1,t72_funct_1,t72_funct_1,t72_funct_1,t72_funct_1,t72_funct_1,t72_funct_1,d5_funct_1,d3_xboole_0,d3_xboole_0,t50_borsuk_1,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,d3_seq_1,d5_seq_1,d5_seq_1,t9_xreal_1,t2_complex1,t11_topreal3,d1_partfun3,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d5_funct_1,d3_xboole_0,d3_xboole_0,t50_borsuk_1,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,d4_seq_1,t13_funcop_1,d3_seq_1,d5_seq_1,d5_seq_1,t26_toprns_1,t3_brouwer,t8_topreal9,t77_square_1,t46_jgraph_1,t8_topreal3,t8_topreal3,t11_xreal_1,d3_partfun3,t24_topmetr,d5_abian,d4_brouwer,d4_abian,d3_xboole_0,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,t33_zfmisc_1,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d1_funct_2,d3_seq_1,d5_seq_1,d5_seq_1,d5_seq_1,d5_seq_1,d3_seq_1,d5_seq_1,d4_seq_1,t13_funcop_1,d3_seq_1,d5_seq_1,d5_seq_1,d1_funct_2,d5_partfun3,d4_seq_1,d5_seq_1,d1_funct_2,d4_rfunct_1,d9_xcmplx_0,d3_seq_1,d7_seq_1,d3_seq_1,d5_seq_1,d3_seq_1,d5_seq_1,d5_brouwer,t8_brouwer,d16_euclid,d2_topreala,t69_funct_3,t21_funct_2,t83_topreal6,t41_yellow12,t2_topmetr,d5_abian,d4_abian,d3_xboole_0,t32_tops_2,t70_tops_2,t56_topreala,t25_topgrp_1,d1_funct_2,d1_funct_2,t46_relat_1,d5_tops_2,t56_topreala,t55_relat_1,t65_tops_2,t71_relat_1,t46_relat_1,d5_funct_1,t23_funct_1,t35_funct_1,t9_funct_1,d3_xboole_0,t43_funct_2,t23_funct_1,t20_jgraph_2,t32_tops_2,t45_borsuk_1,d3_xboole_0,d4_tarski,t17_xboole_1,t32_tops_2,t106_zfmisc_1,d3_xboole_0,t20_jgraph_2,t106_zfmisc_1,d3_xboole_0,d3_xboole_0,t38_tops_1,d3_tarski,t116_funct_2,t2_topmetr,d3_xboole_0,d3_xboole_0,d5_abian,d4_abian,d3_xboole_0,d3_xboole_0,t43_funct_2,d3_xboole_0,d2_zfmisc_1,d3_xboole_0,t43_funct_2,d4_tops_2,t62_tops_2,t92_zfmisc_1,t27_xboole_1,t156_relat_1,t43_funct_2,t21_funct_2,l1_brouwer,t1_partfun3,d3_xboole_0,t20_jgraph_2]), [file(brouwer,t13_brouwer),interesting(0.82)]). fof(t15_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v3_xreal_0(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(k2_brouwer(2,B,A)),u1_struct_0(k2_brouwer(2,B,A))) & v5_pre_topc(C,k2_brouwer(2,B,A),k2_brouwer(2,B,A)) & m2_relset_1(C,u1_struct_0(k2_brouwer(2,B,A)),u1_struct_0(k2_brouwer(2,B,A))) ) => ? [D] : ( m1_subset_1(D,u1_struct_0(k2_brouwer(2,B,A))) & k8_funct_2(u1_struct_0(k2_brouwer(2,B,A)),u1_struct_0(k2_brouwer(2,B,A)),C,D) = D ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_brouwer,d5_abian,d3_abian,d3_abian]), [file(brouwer,t15_brouwer),interesting(0.82)]). fof(t10_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & v2_xreal_0(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ! [C] : ( ( ~ v3_struct_0(C) & m1_pre_topc(C,k2_brouwer(2,B,A)) ) => ~ ( C = k7_toprealb(2,B,A) & r1_borsuk_1(k2_brouwer(2,B,A),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_borsuk_1,t9_toprealb,t17_topreal9,t3_brouwer,t6_borsuk_2,d17_borsuk_1,d18_borsuk_1,t13_funcop_1,d2_borsuk_2,t48_topalg_1,t1_topalg_2,t2_topalg_2,d7_borsuk_2,d7_borsuk_2,t58_tops_2,t21_funct_2,d19_borsuk_1,t21_funct_2,d19_borsuk_1,t21_funct_2,d19_borsuk_1,t21_funct_2,d19_borsuk_1,t47_topalg_1,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,d1_topalg_1,d5_eqrel_1,d3_topalg_1]), [file(brouwer,t10_brouwer),interesting(0.71)]). fof(l19_brouwer,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,k1_numbers) => v9_pscomp_1(k1_borsuk_1(k1_numbers,u1_struct_0(A),B),A) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t14_funcop_1,d25_pscomp_1,t37_zfmisc_1,t168_relat_1,t28_xboole_1,t169_relat_1,t12_pre_topc,t56_zfmisc_1,t168_relat_1,d7_xboole_0,t171_relat_1]), [file(brouwer,l19_brouwer),interesting(0.71)]). fof(t2_brouwer,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => k2_topreal9(A,B,0) = k1_struct_0(k15_euclid(A),B) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t8_topreal9,t26_toprns_1,t29_toprns_1,d1_tarski,d10_xboole_0,d3_tarski,d1_tarski,t29_toprns_1,t8_topreal9]), [file(brouwer,t2_brouwer),interesting(0.70)]). fof(l1_brouwer,theorem,( k2_pre_topc(k15_euclid(2)) = u1_struct_0(k15_euclid(2)) ), inference(mizar_proof,[status(thm)],[t12_pre_topc]), [file(brouwer,l1_brouwer),interesting(0.68)]). fof(t3_brouwer,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => u1_struct_0(k2_brouwer(A,C,B)) = k2_topreal9(A,C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_pre_topc,t12_pre_topc]), [file(brouwer,t3_brouwer),interesting(0.62)]). fof(t9_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v3_xreal_0(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m2_subset_1(B,k1_numbers,k5_numbers) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k2_brouwer(B,C,A))) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k2_brouwer(B,C,A))) & m2_relset_1(E,u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k2_brouwer(B,C,A))) ) => ( m1_subset_1(D,u1_struct_0(k7_toprealb(B,C,A))) => ( r2_abian(u1_struct_0(k2_brouwer(B,C,A)),D,E) | k4_brouwer(B,C,A,D,E) = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_abian,d4_brouwer,t28_topreal9,t9_toprealb,d3_xboole_0,d3_brouwer]), [file(brouwer,t9_brouwer),interesting(0.48)]). fof(t11_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v3_xreal_0(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m2_subset_1(B,k1_numbers,k5_numbers) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k2_brouwer(B,C,A))) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k2_brouwer(B,C,A))) & m2_relset_1(E,u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k2_brouwer(B,C,A))) ) => ( m1_subset_1(D,u1_struct_0(k7_toprealb(B,C,A))) => ( r2_abian(u1_struct_0(k2_brouwer(B,C,A)),D,E) | k8_funct_2(u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k7_toprealb(B,C,A)),k5_brouwer(B,A,C,E),D) = D ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_brouwer,t9_brouwer]), [file(brouwer,t11_brouwer),interesting(0.48)]). fof(t6_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v3_xreal_0(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m2_subset_1(B,k1_numbers,k5_numbers) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(B))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(B))) => ( ( m1_subset_1(C,u1_struct_0(k2_brouwer(B,D,A))) & m1_subset_1(E,u1_struct_0(k2_brouwer(B,D,A))) ) => ( C = E | m1_subset_1(k3_brouwer(B,D,C,E,A),u1_struct_0(k7_toprealb(B,D,A))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_toprealb,d3_brouwer,d3_xboole_0]), [file(brouwer,t6_brouwer),interesting(0.38)]). fof(t4_brouwer,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_xreal_0(B) & ~ v3_xreal_0(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ~ ( C != D & m1_subset_1(C,u1_struct_0(k2_brouwer(A,E,B))) & ~ m1_subset_1(C,u1_struct_0(k7_toprealb(A,E,B))) & ! [F] : ( m1_subset_1(F,u1_struct_0(k7_toprealb(A,E,B))) => k1_tarski(F) != k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,C,D),k3_topreal9(A,E,B)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_toprealb,t3_brouwer,t9_topreal9,t25_euclid,t8_topreal9,d5_real_1,t7_topreal9,t37_topreal9,d1_tarski,d3_xboole_0]), [file(brouwer,t4_brouwer),interesting(0.34)]). fof(t5_brouwer,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_xreal_0(B) & ~ v3_xreal_0(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ~ ( C != D & r2_hidden(C,u1_struct_0(k7_toprealb(A,E,B))) & m1_subset_1(D,u1_struct_0(k2_brouwer(A,E,B))) & ! [F] : ( m1_subset_1(F,u1_struct_0(k7_toprealb(A,E,B))) => ~ ( F != C & k2_tarski(C,F) = k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,C,D),k3_topreal9(A,E,B)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_toprealb,t25_euclid,t3_brouwer,t38_topreal9,d2_tarski,d3_xboole_0]), [file(brouwer,t5_brouwer),interesting(0.33)]). fof(t12_brouwer,theorem,( ! [A] : ( ( v1_xreal_0(A) & ~ v3_xreal_0(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m2_subset_1(B,k1_numbers,k5_numbers) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(B))) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k2_brouwer(B,C,A))) & v5_pre_topc(D,k2_brouwer(B,C,A),k2_brouwer(B,C,A)) & m2_relset_1(D,u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k2_brouwer(B,C,A))) ) => ( ~ r3_abian(D) => k2_partfun1(u1_struct_0(k2_brouwer(B,C,A)),u1_struct_0(k7_toprealb(B,C,A)),k5_brouwer(B,A,C,D),k3_topreal9(B,C,A)) = k7_grcat_1(k7_toprealb(B,C,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t3_brouwer,t17_topreal9,t91_relat_1,d11_grcat_1,t71_relat_1,t9_toprealb,d5_abian,t72_funct_1,t11_brouwer,t11_grcat_1,t9_funct_1]), [file(brouwer,t12_brouwer),interesting(0.29)]). fof(t8_brouwer,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_xreal_0(B) & ~ v3_xreal_0(B) ) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ! [E] : ( v1_xreal_0(E) => ! [F] : ( v1_xreal_0(F) => ! [G] : ( m1_subset_1(G,u1_struct_0(k15_euclid(2))) => ! [H] : ( m1_subset_1(H,u1_struct_0(k15_euclid(2))) => ! [I] : ( m1_subset_1(I,u1_struct_0(k15_euclid(2))) => ( ( m1_subset_1(G,u1_struct_0(k2_brouwer(2,I,B))) & m1_subset_1(H,u1_struct_0(k2_brouwer(2,I,B))) & C = k5_real_1(k21_euclid(H),k21_euclid(G)) & D = k5_real_1(k22_euclid(H),k22_euclid(G)) & E = k5_real_1(k21_euclid(G),k21_euclid(I)) & F = k5_real_1(k22_euclid(G),k22_euclid(I)) & A = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(E,C),k3_xcmplx_0(F,D))),k8_square_1(k6_xcmplx_0(k5_square_1(k2_xcmplx_0(k3_xcmplx_0(E,C),k3_xcmplx_0(F,D))),k3_xcmplx_0(k2_xcmplx_0(k5_square_1(C),k5_square_1(D)),k6_xcmplx_0(k2_xcmplx_0(k5_square_1(E),k5_square_1(F)),k5_square_1(B)))))),k2_xcmplx_0(k5_square_1(C),k5_square_1(D))) ) => ( G = H | k3_brouwer(2,I,G,H,B) = k23_euclid(k2_xcmplx_0(k21_euclid(G),k3_xcmplx_0(A,C)),k2_xcmplx_0(k22_euclid(G),k3_xcmplx_0(A,D))) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_brouwer,d3_xboole_0,t26_topreal9,t54_euclid,t33_euclid,t9_jordan2c,t49_euclid,t53_euclid,t7_topreal3,t9_topreal3,t8_topreal3,t7_topreal3,t9_topreal3,t8_topreal3,t11_topreal3,t74_square_1,t10_xreal_1,d1_quin_1,d1_quin_1,d3_xboole_0,t9_topreal9,t46_jgraph_1,t8_topreal3,t8_topreal3,t41_topreal9,t42_topreal9,d2_polyeq_1,t26_toprns_1,t3_brouwer,t8_topreal9,t77_square_1,t46_jgraph_1,t8_topreal3,t8_topreal3,t11_xreal_1,t133_xreal_1,t26_xreal_1,t9_xreal_1,t97_square_1,t85_square_1,t92_xcmplx_1,t131_xreal_1,t133_xreal_1,t174_real_2,t5_polyeq_1,d2_polyeq_1,t16_quin_1,d3_polyeq_1,t11_polyeq_1,t131_xreal_1,t73_real_1,t11_xreal_1,t8_xreal_1,d4_square_1,t9_xreal_1,t128_real_2,t57_euclid,t135_xreal_1,t57_euclid,t33_euclid,t31_euclid,d3_brouwer,t134_xreal_1,t89_square_1,t128_real_2,t90_square_1,t57_euclid]), [file(brouwer,t8_brouwer),interesting(0.25)]). fof(d1_funct_2,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => ( v1_funct_2(C,A,B) <=> A = k4_relset_1(A,B,C) ) ) & ( B = k1_xboole_0 => ( A = k1_xboole_0 | ( v1_funct_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ), file(funct_2,d1_funct_2), [interesting(0.00)]). fof(d10_pre_topc,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( ( v1_pre_topc(C) & m1_pre_topc(C,A) ) => ( C = k3_pre_topc(A,B) <=> k2_pre_topc(C) = B ) ) ) ) ), file(pre_topc,d10_pre_topc), [interesting(0.00)]). fof(t12_pre_topc,theorem,( ! [A] : ( l1_struct_0(A) => k2_pre_topc(A) = u1_struct_0(A) ) ), file(pre_topc,t12_pre_topc), [interesting(0.00)]). fof(t17_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r1_tarski(k3_topreal9(A,C,B),k2_topreal9(A,C,B)) ) ) ) ), file(topreal9,t17_topreal9), [interesting(0.00)]). fof(t91_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => k1_relat_1(k7_relat_1(B,A)) = A ) ) ), file(relat_1,t91_relat_1), [interesting(0.00)]). fof(d11_grcat_1,definition,( ! [A] : ( l1_struct_0(A) => k7_grcat_1(A) = k6_partfun1(u1_struct_0(A)) ) ), file(grcat_1,d11_grcat_1), [interesting(0.00)]). fof(t71_relat_1,theorem,( ! [A] : ( k1_relat_1(k6_relat_1(A)) = A & k2_relat_1(k6_relat_1(A)) = A ) ), file(relat_1,t71_relat_1), [interesting(0.00)]). fof(t9_toprealb,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => u1_struct_0(k7_toprealb(A,C,B)) = k3_topreal9(A,C,B) ) ) ) ), file(toprealb,t9_toprealb), [interesting(0.00)]). fof(d5_abian,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( r3_abian(A) <=> ? [B] : r1_abian(B,A) ) ) ), file(abian,d5_abian), [interesting(0.00)]). fof(t72_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,A) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t72_funct_1), [interesting(0.00)]). fof(d5_brouwer,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( ( v1_xreal_0(B) & ~ v3_xreal_0(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(k2_brouwer(A,C,B)),u1_struct_0(k2_brouwer(A,C,B))) & m2_relset_1(D,u1_struct_0(k2_brouwer(A,C,B)),u1_struct_0(k2_brouwer(A,C,B))) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k2_brouwer(A,C,B)),u1_struct_0(k7_toprealb(A,C,B))) & m2_relset_1(E,u1_struct_0(k2_brouwer(A,C,B)),u1_struct_0(k7_toprealb(A,C,B))) ) => ( E = k5_brouwer(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k2_brouwer(A,C,B))) => k8_funct_2(u1_struct_0(k2_brouwer(A,C,B)),u1_struct_0(k7_toprealb(A,C,B)),E,F) = k4_brouwer(A,C,B,F,D) ) ) ) ) ) ) ) ), file(brouwer,d5_brouwer), [interesting(0.00)]). fof(d4_abian,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,A) & m2_relset_1(C,A,A) ) => ( r2_abian(A,B,C) <=> B = k8_funct_2(A,A,C,B) ) ) ) ) ), file(abian,d4_abian), [interesting(0.00)]). fof(d4_brouwer,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( ( v1_xreal_0(C) & ~ v3_xreal_0(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(k2_brouwer(A,B,C))) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k2_brouwer(A,B,C)),u1_struct_0(k2_brouwer(A,B,C))) & m2_relset_1(E,u1_struct_0(k2_brouwer(A,B,C)),u1_struct_0(k2_brouwer(A,B,C))) ) => ( ~ r2_abian(u1_struct_0(k2_brouwer(A,B,C)),D,E) => ! [F] : ( m1_subset_1(F,u1_struct_0(k7_toprealb(A,B,C))) => ( F = k4_brouwer(A,B,C,D,E) <=> ? [G] : ( m1_subset_1(G,u1_struct_0(k15_euclid(A))) & ? [H] : ( m1_subset_1(H,u1_struct_0(k15_euclid(A))) & G = D & H = k8_funct_2(u1_struct_0(k2_brouwer(A,B,C)),u1_struct_0(k2_brouwer(A,B,C)),E,D) & F = k3_brouwer(A,B,H,G,C) ) ) ) ) ) ) ) ) ) ) ), file(brouwer,d4_brouwer), [interesting(0.00)]). fof(t28_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r2_hidden(B,k4_topreal9(A,C,B)) ) ) ) ), file(topreal9,t28_topreal9), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d3_brouwer,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( ( v1_xreal_0(E) & ~ v3_xreal_0(E) ) => ( ( m1_subset_1(C,u1_struct_0(k2_brouwer(A,B,E))) & m1_subset_1(D,u1_struct_0(k2_brouwer(A,B,E))) ) => ( C = D | ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(A))) => ( F = k3_brouwer(A,B,C,D,E) <=> ( r2_hidden(F,k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,C,D),k3_topreal9(A,B,E))) & F != C ) ) ) ) ) ) ) ) ) ) ), file(brouwer,d3_brouwer), [interesting(0.00)]). fof(t11_grcat_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k8_funct_2(u1_struct_0(A),u1_struct_0(A),k7_grcat_1(A),B) = B ) ) ), file(grcat_1,t11_grcat_1), [interesting(0.00)]). fof(t9_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) => A = B ) ) ) ), file(funct_1,t9_funct_1), [interesting(0.00)]). fof(t4_tsep_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_pre_topc(B,A) => ! [C] : ( m1_pre_topc(C,A) => ( r1_tarski(u1_struct_0(B),u1_struct_0(C)) <=> m1_pre_topc(B,C) ) ) ) ) ), file(tsep_1,t4_tsep_1), [interesting(0.00)]). fof(d20_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ( r1_borsuk_1(A,B) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & v5_pre_topc(C,A,B) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) & v3_borsuk_1(C,A,B) ) ) ) ) ), file(borsuk_1,d20_borsuk_1), [interesting(0.00)]). fof(t6_borsuk_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( ( v5_seqm_3(C) & m1_borsuk_2(C,A,B,B) ) => C = k3_borsuk_1(k5_topmetr,A,B) ) ) ) ), file(borsuk_2,t6_borsuk_2), [interesting(0.00)]). fof(d17_borsuk_1,definition,( k23_borsuk_1 = 0 ), file(borsuk_1,d17_borsuk_1), [interesting(0.00)]). fof(d18_borsuk_1,definition,( k24_borsuk_1 = 1 ), file(borsuk_1,d18_borsuk_1), [interesting(0.00)]). fof(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [interesting(0.00)]). fof(d2_borsuk_2,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_borsuk_2(A,B,C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(k5_topmetr),u1_struct_0(A)) & m2_relset_1(D,u1_struct_0(k5_topmetr),u1_struct_0(A)) ) => ( m1_borsuk_2(D,A,B,C) <=> ( v5_pre_topc(D,k5_topmetr,A) & k1_funct_1(D,0) = B & k1_funct_1(D,1) = C ) ) ) ) ) ) ) ), file(borsuk_2,d2_borsuk_2), [interesting(0.00)]). fof(t48_topalg_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( r2_hidden(C,u1_struct_0(k3_topalg_1(A,B))) <=> ? [D] : ( m1_borsuk_2(D,A,B,B) & C = k6_eqrel_1(k1_topalg_1(A,B),k2_topalg_1(A,B),D) ) ) ) ) ), file(topalg_1,t48_topalg_1), [interesting(0.00)]). fof(t1_topalg_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,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(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ! [G] : ( m1_borsuk_2(G,B,E,F) => ( ( C = E & D = F & r1_borsuk_6(B,E,F) ) => m1_borsuk_2(G,A,C,D) ) ) ) ) ) ) ) ) ), file(topalg_2,t1_topalg_2), [interesting(0.00)]). fof(t2_topalg_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v1_topalg_2(B,A) & m1_pre_topc(B,k15_euclid(A)) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_borsuk_2(E,B,C,D) => ! [F] : ( m1_borsuk_2(F,B,C,D) => r4_borsuk_2(B,C,D,E,F) ) ) ) ) ) ) ), file(topalg_2,t2_topalg_2), [interesting(0.00)]). fof(d7_borsuk_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( m1_borsuk_2(E,A,B,C) => ( r3_borsuk_2(A,B,C,D,E) <=> ? [F] : ( v1_funct_1(F) & v1_funct_2(F,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(A)) & m2_relset_1(F,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(A)) & v5_pre_topc(F,k6_borsuk_1(k5_topmetr,k5_topmetr),A) & ! [G] : ( m1_subset_1(G,u1_struct_0(k5_topmetr)) => ( k1_binop_1(F,G,0) = k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(A),D,G) & k1_binop_1(F,G,1) = k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(A),E,G) & ! [H] : ( m1_subset_1(H,u1_struct_0(k5_topmetr)) => ( k1_binop_1(F,0,H) = B & k1_binop_1(F,1,H) = C ) ) ) ) ) ) ) ) ) ) ) ), file(borsuk_2,d7_borsuk_2), [interesting(0.00)]). fof(t58_tops_2,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( l1_pre_topc(B) => ! [C] : ( ( ~ v3_struct_0(C) & l1_pre_topc(C) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),u1_struct_0(C)) & m2_relset_1(D,u1_struct_0(A),u1_struct_0(C)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(C),u1_struct_0(B)) & m2_relset_1(E,u1_struct_0(C),u1_struct_0(B)) ) => ( ( v5_pre_topc(D,A,C) & v5_pre_topc(E,C,B) ) => v5_pre_topc(k7_funct_2(u1_struct_0(A),u1_struct_0(C),u1_struct_0(B),D,E),A,B) ) ) ) ) ) ) ), file(tops_2,t58_tops_2), [interesting(0.00)]). fof(t21_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_relat_1(E) & v1_funct_1(E) ) => ( r2_hidden(C,A) => ( B = k1_xboole_0 | k1_funct_1(k5_relat_1(D,E),C) = k1_funct_1(E,k1_funct_1(D,C)) ) ) ) ) ), file(funct_2,t21_funct_2), [interesting(0.00)]). fof(d19_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( v3_borsuk_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,u1_struct_0(B)) => k8_funct_2(u1_struct_0(A),u1_struct_0(B),C,D) = D ) ) ) ) ) ) ), file(borsuk_1,d19_borsuk_1), [interesting(0.00)]). fof(t47_topalg_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_borsuk_2(C,A,B,B) => ! [D] : ( m1_borsuk_2(D,A,B,B) => ( k6_eqrel_1(k1_topalg_1(A,B),k2_topalg_1(A,B),C) = k6_eqrel_1(k1_topalg_1(A,B),k2_topalg_1(A,B),D) <=> r3_borsuk_2(A,B,B,C,D) ) ) ) ) ) ), file(topalg_1,t47_topalg_1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). 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.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(d1_topalg_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( C = k1_topalg_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> m1_borsuk_2(D,A,B,B) ) ) ) ) ), file(topalg_1,d1_topalg_1), [interesting(0.00)]). fof(d5_eqrel_1,definition,( ! [A,B] : ( ( v3_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,A,A) & m2_relset_1(B,A,A) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A))) => ( C = k7_eqrel_1(A,B) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( r2_hidden(D,C) <=> ? [E] : ( r2_hidden(E,A) & D = k6_eqrel_1(A,B,E) ) ) ) ) ) ) ), file(eqrel_1,d5_eqrel_1), [interesting(0.00)]). fof(d3_topalg_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( ( v1_group_1(C) & l1_group_1(C) ) => ( C = k3_topalg_1(A,B) <=> ( u1_struct_0(C) = k8_eqrel_1(k1_topalg_1(A,B),k2_topalg_1(A,B)) & ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ? [F] : ( m1_borsuk_2(F,A,B,B) & ? [G] : ( m1_borsuk_2(G,A,B,B) & D = k6_eqrel_1(k1_topalg_1(A,B),k2_topalg_1(A,B),F) & E = k6_eqrel_1(k1_topalg_1(A,B),k2_topalg_1(A,B),G) & k1_binop_1(u1_group_1(C),D,E) = k6_eqrel_1(k1_topalg_1(A,B),k2_topalg_1(A,B),k1_borsuk_2(A,B,B,B,F,G)) ) ) ) ) ) ) ) ) ) ), file(topalg_1,d3_topalg_1), [interesting(0.00)]). fof(t25_borsuk_3,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_pre_topc(C,A) => ! [D] : ( m1_pre_topc(D,B) => m1_pre_topc(k6_borsuk_1(C,D),k6_borsuk_1(A,B)) ) ) ) ) ), file(borsuk_3,t25_borsuk_3), [interesting(0.00)]). fof(t1_tsep_1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_pre_topc(B,A) => m1_subset_1(u1_struct_0(B),k1_zfmisc_1(u1_struct_0(A))) ) ) ), file(tsep_1,t1_tsep_1), [interesting(0.00)]). fof(t27_xboole_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k3_xboole_0(A,C),k3_xboole_0(B,D)) ) ), file(xboole_1,t27_xboole_1), [interesting(0.00)]). fof(t2_topmetr,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => m1_subset_1(C,u1_struct_0(A)) ) ) ) ), file(topmetr,t2_topmetr), [interesting(0.00)]). fof(t46_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => k20_euclid(A,B,B) = k16_euclid(A) ) ) ), file(euclid,t46_euclid), [interesting(0.00)]). fof(t24_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k5_toprns_1(A,k16_euclid(A)) = 0 ) ), file(toprns_1,t24_toprns_1), [interesting(0.00)]). fof(t8_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k2_topreal9(A,D,B)) <=> r1_xreal_0(k5_toprns_1(A,k20_euclid(A,C,D)),B) ) ) ) ) ) ), file(topreal9,t8_topreal9), [interesting(0.00)]). fof(t106_zfmisc_1,theorem,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), [interesting(0.00)]). fof(d5_borsuk_1,definition,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( ( v1_pre_topc(C) & v2_pre_topc(C) & l1_pre_topc(C) ) => ( C = k6_borsuk_1(A,B) <=> ( u1_struct_0(C) = k2_zfmisc_1(u1_struct_0(A),u1_struct_0(B)) & u1_pre_topc(C) = a_3_0_borsuk_1(A,B,C) ) ) ) ) ) ), file(borsuk_1,d5_borsuk_1), [interesting(0.00)]). fof(t19_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => r1_xboole_0(k1_topreal9(A,C,B),k3_topreal9(A,C,B)) ) ) ) ), file(topreal9,t19_topreal9), [interesting(0.00)]). fof(t7_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k1_topreal9(A,D,B)) <=> ~ r1_xreal_0(B,k5_toprns_1(A,k20_euclid(A,C,D))) ) ) ) ) ) ), file(topreal9,t7_topreal9), [interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(t50_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_borsuk_1(A,B))) => ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & C = k8_borsuk_1(A,B,D,E) ) ) ) ) ) ), file(borsuk_1,t50_borsuk_1), [interesting(0.00)]). fof(s1_pscomp_1,theorem, ( ! [A] : ~ ( r2_hidden(A,u1_struct_0(f1_s1_pscomp_1)) & ! [B] : ( m1_subset_1(B,k1_numbers) => ~ p1_s1_pscomp_1(A,B) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(f1_s1_pscomp_1),k1_numbers) & m2_relset_1(A,u1_struct_0(f1_s1_pscomp_1),k1_numbers) & ! [B] : ( m1_subset_1(B,u1_struct_0(f1_s1_pscomp_1)) => p1_s1_pscomp_1(B,k2_seq_1(u1_struct_0(f1_s1_pscomp_1),k1_numbers,A,B)) ) ) ), file(pscomp_1,s1_pscomp_1), [interesting(0.00)]). fof(t24_topmetr,theorem,( u1_struct_0(k3_topmetr) = k1_numbers ), file(topmetr,t24_topmetr), [interesting(0.00)]). fof(t62_borsuk_5,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(k1_numbers)) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k3_topmetr))) => ( A = B => ( v3_rcomp_1(A) <=> v3_pre_topc(B,k3_topmetr) ) ) ) ) ), file(borsuk_5,t62_borsuk_5), [interesting(0.00)]). fof(t40_rcomp_1,theorem,( ! [A] : ( ( v3_rcomp_1(A) & m1_subset_1(A,k1_zfmisc_1(k1_numbers)) ) => ! [B] : ( v1_xreal_0(B) => ~ ( r2_hidden(B,A) & ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & r1_tarski(k2_rcomp_1(k6_xcmplx_0(B,C),k2_xcmplx_0(B,C)),A) ) ) ) ) ) ), file(rcomp_1,t40_rcomp_1), [interesting(0.00)]). fof(d1_xreal_0,definition,( ! [A] : ( v1_xreal_0(A) <=> r2_hidden(A,k1_numbers) ) ), file(xreal_0,d1_xreal_0), [interesting(0.00)]). fof(t57_euclid,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => A = k23_euclid(k21_euclid(A),k22_euclid(A)) ) ), file(euclid,t57_euclid), [interesting(0.00)]). fof(t8_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(t92_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k6_xcmplx_0(A,D),k6_xcmplx_0(B,C)) ) & ~ ( ( ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) ) | ( r1_xreal_0(A,B) & ~ r1_xreal_0(D,C) ) ) & r1_xreal_0(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ) ), file(real_1,t92_real_1), [interesting(0.00)]). fof(d2_zfmisc_1,definition,( ! [A,B,C] : ( C = k2_zfmisc_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E,F] : ( r2_hidden(E,A) & r2_hidden(F,B) & D = k4_tarski(E,F) ) ) ) ), file(zfmisc_1,d2_zfmisc_1), [interesting(0.00)]). fof(t66_pscomp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( A = a_2_2_pscomp_1(B,C) => v3_pre_topc(A,k15_euclid(2)) ) ) ) ) ), file(pscomp_1,t66_pscomp_1), [interesting(0.00)]). fof(t46_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( ( v3_pre_topc(C,A) & v3_pre_topc(D,B) ) => v3_pre_topc(k7_borsuk_1(A,B,C,D),k6_borsuk_1(A,B)) ) ) ) ) ) ), file(borsuk_1,t46_borsuk_1), [interesting(0.00)]). fof(t116_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ~ ( r2_hidden(E,k2_funct_2(A,B,D,C)) & ! [F] : ( m1_subset_1(F,A) => ~ ( r2_hidden(F,C) & E = k1_funct_1(D,F) ) ) ) ) ), file(funct_2,t116_funct_2), [interesting(0.00)]). fof(t56_euclid,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( k21_euclid(k23_euclid(A,B)) = A & k22_euclid(k23_euclid(A,B)) = B ) ) ) ), file(euclid,t56_euclid), [interesting(0.00)]). fof(t11_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t11_xreal_1), [interesting(0.00)]). fof(t47_rcomp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r2_hidden(C,k2_rcomp_1(A,B)) <=> ( ~ r1_xreal_0(C,A) & ~ r1_xreal_0(B,C) ) ) ) ) ) ), file(rcomp_1,t47_rcomp_1), [interesting(0.00)]). fof(t20_jgraph_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( v5_pre_topc(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(B))) => ~ ( r2_hidden(k8_funct_2(u1_struct_0(A),u1_struct_0(B),C,D),E) & v3_pre_topc(E,B) & ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r2_hidden(D,F) & v3_pre_topc(F,A) & r1_tarski(k4_pre_topc(A,B,C,F),E) ) ) ) ) ) ) ) ) ) ), file(jgraph_2,t20_jgraph_2), [interesting(0.00)]). fof(t83_topreal6,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(A),k1_numbers) & m2_relset_1(B,u1_struct_0(A),k1_numbers) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(k3_topmetr)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(k3_topmetr)) ) => ( B = C => ( v9_pscomp_1(B,A) <=> v5_pre_topc(C,A,k3_topmetr) ) ) ) ) ) ), file(topreal6,t83_topreal6), [interesting(0.00)]). fof(t68_pscomp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( A = a_2_4_pscomp_1(B,C) => v3_pre_topc(A,k15_euclid(2)) ) ) ) ) ), file(pscomp_1,t68_pscomp_1), [interesting(0.00)]). fof(t73_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,0) => ( ~ ( ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) ) & ~ ( ~ r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) & r1_xreal_0(C,B) ) ) ) ) ) ) ), file(real_1,t73_real_1), [interesting(0.00)]). fof(t9_seq_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ~ r1_xreal_0(B,k4_xcmplx_0(A)) & ~ r1_xreal_0(A,B) ) <=> ~ r1_xreal_0(A,k18_complex1(B)) ) ) ) ), file(seq_2,t9_seq_2), [interesting(0.00)]). fof(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(t143_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => r1_xreal_0(k17_complex1(k6_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ), file(complex1,t143_complex1), [interesting(0.00)]). fof(t138_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ), file(complex1,t138_complex1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(t8_rcomp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r2_hidden(A,k2_rcomp_1(k6_xcmplx_0(B,C),k2_xcmplx_0(B,C))) <=> ~ r1_xreal_0(C,k18_complex1(k6_xcmplx_0(A,B))) ) ) ) ) ), file(rcomp_1,t8_rcomp_1), [interesting(0.00)]). fof(t14_funcop_1,theorem,( ! [A,B] : ( A != k1_xboole_0 => k2_relat_1(k2_funcop_1(A,B)) = k1_tarski(B) ) ), file(funcop_1,t14_funcop_1), [interesting(0.00)]). fof(d25_pscomp_1,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(A),k1_numbers) & m2_relset_1(B,u1_struct_0(A),k1_numbers) ) => ( v9_pscomp_1(B,A) <=> ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_numbers)) => ( v2_rcomp_1(C) => v4_pre_topc(k11_pscomp_1(A,B,C),A) ) ) ) ) ) ), file(pscomp_1,d25_pscomp_1), [interesting(0.00)]). fof(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(t168_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => k10_relat_1(B,A) = k10_relat_1(B,k3_xboole_0(k2_relat_1(B),A)) ) ), file(relat_1,t168_relat_1), [interesting(0.00)]). fof(t28_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k3_xboole_0(A,B) = A ) ), file(xboole_1,t28_xboole_1), [interesting(0.00)]). fof(t169_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => k10_relat_1(A,k2_relat_1(A)) = k1_relat_1(A) ) ), file(relat_1,t169_relat_1), [interesting(0.00)]). fof(t56_zfmisc_1,theorem,( ! [A,B] : ( ~ r2_hidden(A,B) => r1_xboole_0(k1_tarski(A),B) ) ), file(zfmisc_1,t56_zfmisc_1), [interesting(0.00)]). fof(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(t171_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => k10_relat_1(A,k1_xboole_0) = k1_xboole_0 ) ), file(relat_1,t171_relat_1), [interesting(0.00)]). fof(t1_jordan1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => u1_struct_0(k3_pre_topc(A,B)) = B ) ) ), file(jordan1,t1_jordan1), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(t33_zfmisc_1,theorem,( ! [A,B,C,D] : ( k4_tarski(A,B) = k4_tarski(C,D) => ( A = C & B = D ) ) ), file(zfmisc_1,t33_zfmisc_1), [interesting(0.00)]). fof(d3_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k3_seq_1(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k3_real_1(k1_seq_1(A,D),k1_seq_1(B,D)) ) ) ) ) ) ) ), file(seq_1,d3_seq_1), [interesting(0.00)]). fof(d5_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k5_seq_1(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k4_real_1(k1_seq_1(A,D),k1_seq_1(B,D)) ) ) ) ) ) ) ), file(seq_1,d5_seq_1), [interesting(0.00)]). fof(t9_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_1), [interesting(0.00)]). fof(t2_complex1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( k2_xcmplx_0(k5_square_1(A),k5_square_1(B)) = 0 <=> ( A = 0 & B = 0 ) ) ) ) ), file(complex1,t2_complex1), [interesting(0.00)]). fof(t11_topreal3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ( ( k21_euclid(A) = k21_euclid(B) & k22_euclid(A) = k22_euclid(B) ) => A = B ) ) ) ), file(topreal3,t11_topreal3), [interesting(0.00)]). fof(d1_partfun3,definition,( ! [A] : ( v1_relat_1(A) => ( v1_partfun3(A) <=> ! [B] : ( v1_xreal_0(B) => ~ ( r2_hidden(B,k2_relat_1(A)) & r1_xreal_0(B,0) ) ) ) ) ), file(partfun3,d1_partfun3), [interesting(0.00)]). fof(d4_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k4_seq_1(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k5_real_1(k1_seq_1(A,D),k1_seq_1(B,D)) ) ) ) ) ) ) ), file(seq_1,d4_seq_1), [interesting(0.00)]). fof(t26_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => r1_xreal_0(0,k5_toprns_1(A,B)) ) ) ), file(toprns_1,t26_toprns_1), [interesting(0.00)]). fof(t77_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,B) ) => r1_xreal_0(k5_square_1(A),k5_square_1(B)) ) ) ) ), file(square_1,t77_square_1), [interesting(0.00)]). fof(t46_jgraph_1,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => k7_square_1(k5_toprns_1(2,A)) = k3_real_1(k7_square_1(k21_euclid(A)),k7_square_1(k22_euclid(A))) ) ), file(jgraph_1,t46_jgraph_1), [interesting(0.00)]). fof(t8_topreal3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ( k21_euclid(k20_euclid(2,A,B)) = k5_real_1(k21_euclid(A),k21_euclid(B)) & k22_euclid(k20_euclid(2,A,B)) = k5_real_1(k22_euclid(A),k22_euclid(B)) ) ) ) ), file(topreal3,t8_topreal3), [interesting(0.00)]). fof(d3_partfun3,definition,( ! [A] : ( v1_relat_1(A) => ( v3_partfun3(A) <=> ! [B] : ( v1_xreal_0(B) => ( r2_hidden(B,k2_relat_1(A)) => r1_xreal_0(B,0) ) ) ) ) ), file(partfun3,d3_partfun3), [interesting(0.00)]). fof(d5_partfun3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k1_partfun3(A) <=> ( k1_relat_1(B) = k1_relat_1(A) & ! [C] : ( r2_hidden(C,k1_relat_1(B)) => k1_funct_1(B,C) = k9_square_1(k1_seq_1(A,C)) ) ) ) ) ) ), file(partfun3,d5_partfun3), [interesting(0.00)]). fof(d4_rfunct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_seq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k1_rfunct_1(A,B) <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k4_xboole_0(k1_relat_1(B),k10_relat_1(B,k1_tarski(0)))) & ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k1_funct_1(C,D) = k4_real_1(k1_seq_1(A,D),k2_real_1(k1_seq_1(B,D))) ) ) ) ) ) ) ), file(rfunct_1,d4_rfunct_1), [interesting(0.00)]). fof(d9_xcmplx_0,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ), file(xcmplx_0,d9_xcmplx_0), [interesting(0.00)]). fof(d7_seq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_seq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k15_seq_1(A) <=> ( k1_relat_1(B) = k1_relat_1(A) & ! [C] : ( r2_hidden(C,k1_relat_1(B)) => k1_funct_1(B,C) = k1_real_1(k1_seq_1(A,C)) ) ) ) ) ) ), file(seq_1,d7_seq_1), [interesting(0.00)]). fof(t26_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( r2_hidden(D,k4_topreal9(A,B,C)) <=> ? [E] : ( v1_xreal_0(E) & D = k17_euclid(A,k18_euclid(k6_xcmplx_0(1,E),A,B),k18_euclid(E,A,C)) & r1_xreal_0(0,E) ) ) ) ) ) ), file(topreal9,t26_topreal9), [interesting(0.00)]). fof(t54_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => k18_euclid(k6_xcmplx_0(C,D),A,B) = k20_euclid(A,k18_euclid(C,A,B),k18_euclid(D,A,B)) ) ) ) ) ), file(euclid,t54_euclid), [interesting(0.00)]). fof(t33_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ( k18_euclid(1,A,B) = B & k18_euclid(0,A,B) = k16_euclid(A) ) ) ) ), file(euclid,t33_euclid), [interesting(0.00)]). fof(t9_jordan2c,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k20_euclid(A,k17_euclid(A,B,C),D) = k17_euclid(A,k20_euclid(A,B,D),C) ) ) ) ) ), file(jordan2c,t9_jordan2c), [interesting(0.00)]). fof(t49_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k17_euclid(A,B,k20_euclid(A,C,D)) = k20_euclid(A,k17_euclid(A,B,C),D) ) ) ) ) ), file(euclid,t49_euclid), [interesting(0.00)]). fof(t53_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( v1_xreal_0(D) => k18_euclid(D,A,k20_euclid(A,B,C)) = k20_euclid(A,k18_euclid(D,A,B),k18_euclid(D,A,C)) ) ) ) ) ), file(euclid,t53_euclid), [interesting(0.00)]). fof(t7_topreal3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(2))) => ( k21_euclid(k17_euclid(2,A,B)) = k3_real_1(k21_euclid(A),k21_euclid(B)) & k22_euclid(k17_euclid(2,A,B)) = k3_real_1(k22_euclid(A),k22_euclid(B)) ) ) ) ), file(topreal3,t7_topreal3), [interesting(0.00)]). fof(t9_topreal3,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( v1_xreal_0(B) => ( k21_euclid(k18_euclid(B,2,A)) = k3_xcmplx_0(B,k21_euclid(A)) & k22_euclid(k18_euclid(B,2,A)) = k3_xcmplx_0(B,k22_euclid(A)) ) ) ) ), file(topreal3,t9_topreal3), [interesting(0.00)]). fof(t74_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( 0 != A & r1_xreal_0(k5_square_1(A),0) ) ) ), file(square_1,t74_square_1), [interesting(0.00)]). fof(d1_quin_1,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k1_quin_1(A,B,C) = k6_xcmplx_0(k5_square_1(B),k3_xcmplx_0(k3_xcmplx_0(4,A),C)) ) ) ) ), file(quin_1,d1_quin_1), [interesting(0.00)]). fof(t9_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( r2_hidden(C,k3_topreal9(A,D,B)) <=> k5_toprns_1(A,k20_euclid(A,C,D)) = B ) ) ) ) ) ), file(topreal9,t9_topreal9), [interesting(0.00)]). fof(t41_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(2))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => k21_euclid(k17_euclid(2,k18_euclid(A,2,C),k18_euclid(B,2,D))) = k2_xcmplx_0(k3_xcmplx_0(A,k21_euclid(C)),k3_xcmplx_0(B,k21_euclid(D))) ) ) ) ) ), file(topreal9,t41_topreal9), [interesting(0.00)]). fof(t42_topreal9,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(2))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(2))) => k22_euclid(k17_euclid(2,k18_euclid(A,2,C),k18_euclid(B,2,D))) = k2_xcmplx_0(k3_xcmplx_0(A,k22_euclid(C)),k3_xcmplx_0(B,k22_euclid(D))) ) ) ) ) ), file(topreal9,t42_topreal9), [interesting(0.00)]). fof(d2_polyeq_1,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => k3_polyeq_1(A,B,C,D) = k2_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,k5_square_1(D)),k3_xcmplx_0(B,D)),C) ) ) ) ) ), file(polyeq_1,d2_polyeq_1), [interesting(0.00)]). fof(t133_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(B,0) ) => r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t133_xreal_1), [interesting(0.00)]). fof(t26_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ), file(xreal_1,t26_xreal_1), [interesting(0.00)]). fof(t97_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => k8_square_1(k3_xcmplx_0(A,B)) = k3_xcmplx_0(k8_square_1(A),k8_square_1(B)) ) ) ) ), file(square_1,t97_square_1), [interesting(0.00)]). fof(t85_square_1,theorem,( k9_square_1(4) = 2 ), file(square_1,t85_square_1), [interesting(0.00)]). fof(t92_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ( A != 0 => k7_xcmplx_0(B,C) = k7_xcmplx_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ), file(xcmplx_1,t92_xcmplx_1), [interesting(0.00)]). fof(t131_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t131_xreal_1), [interesting(0.00)]). fof(t174_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,0) => ( r1_xreal_0(k2_xcmplx_0(A,B),B) & r1_xreal_0(B,k6_xcmplx_0(B,A)) ) ) & ( ( r1_xreal_0(k2_xcmplx_0(A,B),B) | r1_xreal_0(B,k6_xcmplx_0(B,A)) ) => r1_xreal_0(A,0) ) ) ) ) ), file(real_2,t174_real_2), [interesting(0.00)]). fof(t5_polyeq_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(0,k1_quin_1(A,B,C)) => ( A = 0 | ! [D] : ( v1_xreal_0(D) => ~ ( k3_polyeq_1(A,B,C,D) = 0 & D != k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)) & D != k7_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)) ) ) ) ) ) ) ) ), file(polyeq_1,t5_polyeq_1), [interesting(0.00)]). fof(t16_quin_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( r1_xreal_0(0,k1_quin_1(A,B,C)) => ( A = 0 | k2_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,k5_square_1(D)),k3_xcmplx_0(B,D)),C) = k3_xcmplx_0(k3_xcmplx_0(A,k6_xcmplx_0(D,k7_xcmplx_0(k6_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)))),k6_xcmplx_0(D,k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(B),k8_square_1(k1_quin_1(A,B,C))),k3_xcmplx_0(2,A)))) ) ) ) ) ) ) ), file(quin_1,t16_quin_1), [interesting(0.00)]). fof(d3_polyeq_1,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => k5_polyeq_1(A,B,C,D) = k3_xcmplx_0(A,k3_xcmplx_0(k6_xcmplx_0(B,C),k6_xcmplx_0(B,D))) ) ) ) ) ), file(polyeq_1,d3_polyeq_1), [interesting(0.00)]). fof(t11_polyeq_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => ! [E] : ( v1_xcmplx_0(E) => ( ! [F] : ( v1_xreal_0(F) => k3_polyeq_1(C,D,E,F) = k5_polyeq_1(C,F,A,B) ) => ( C = 0 | ( k7_xcmplx_0(D,C) = k4_xcmplx_0(k2_xcmplx_0(A,B)) & k7_xcmplx_0(E,C) = k3_xcmplx_0(A,B) ) ) ) ) ) ) ) ) ), file(polyeq_1,t11_polyeq_1), [interesting(0.00)]). fof(d4_square_1,definition,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(0,A) => ! [B] : ( v1_xreal_0(B) => ( B = k8_square_1(A) <=> ( r1_xreal_0(0,B) & k5_square_1(B) = A ) ) ) ) ) ), file(square_1,d4_square_1), [interesting(0.00)]). fof(t128_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) & ~ ( ~ r1_xreal_0(0,k7_xcmplx_0(A,B)) & ~ r1_xreal_0(0,k7_xcmplx_0(B,A)) ) ) ) ) ), file(real_2,t128_real_2), [interesting(0.00)]). fof(t135_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(0,k3_xcmplx_0(A,B)) & ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(0,B) ) & ~ ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(B,0) ) ) ) ) ), file(xreal_1,t135_xreal_1), [interesting(0.00)]). fof(t31_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ( k17_euclid(A,k16_euclid(A),B) = B & k17_euclid(A,B,k16_euclid(A)) = B ) ) ) ), file(euclid,t31_euclid), [interesting(0.00)]). fof(t134_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(0,B) & r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ) ), file(xreal_1,t134_xreal_1), [interesting(0.00)]). fof(t89_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(0,A) => k8_square_1(k5_square_1(A)) = A ) ) ), file(square_1,t89_square_1), [interesting(0.00)]). fof(t90_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(A,0) => k8_square_1(k5_square_1(A)) = k4_xcmplx_0(A) ) ) ), file(square_1,t90_square_1), [interesting(0.00)]). fof(d16_euclid,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => k23_euclid(A,B) = k10_finseq_1(A,B) ) ) ), file(euclid,d16_euclid), [interesting(0.00)]). fof(d2_topreala,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k6_borsuk_1(k3_topalg_2,k3_topalg_2)),u1_struct_0(k15_euclid(2))) & m2_relset_1(A,u1_struct_0(k6_borsuk_1(k3_topalg_2,k3_topalg_2)),u1_struct_0(k15_euclid(2))) ) => ( A = k2_topreala <=> ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => k1_funct_1(A,k4_tarski(B,C)) = k10_finseq_1(B,C) ) ) ) ) ), file(topreala,d2_topreala), [interesting(0.00)]). fof(t69_funct_3,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ( ( k1_relat_1(C) = B & k1_relat_1(D) = B & r2_hidden(A,B) ) => k1_funct_1(k13_funct_3(C,D),A) = k4_tarski(k1_funct_1(C,A),k1_funct_1(D,A)) ) ) ) ), file(funct_3,t69_funct_3), [interesting(0.00)]). fof(t41_yellow12,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( ( ~ v3_struct_0(C) & v2_pre_topc(C) & l1_pre_topc(C) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),u1_struct_0(B)) & v5_pre_topc(D,A,B) & m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(A),u1_struct_0(C)) & v5_pre_topc(E,A,C) & m2_relset_1(E,u1_struct_0(A),u1_struct_0(C)) ) => ( v1_funct_1(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E)) & v1_funct_2(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),u1_struct_0(A),u1_struct_0(k6_borsuk_1(B,C))) & v5_pre_topc(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),A,k6_borsuk_1(B,C)) & m2_relset_1(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),u1_struct_0(A),u1_struct_0(k6_borsuk_1(B,C))) ) ) ) ) ) ) ), file(yellow12,t41_yellow12), [interesting(0.00)]). fof(t32_tops_2,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_pre_topc(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ( v3_pre_topc(C,B) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & v3_pre_topc(D,A) & k3_xboole_0(D,k2_pre_topc(B)) = C ) ) ) ) ) ), file(tops_2,t32_tops_2), [interesting(0.00)]). fof(t70_tops_2,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( ( ~ v3_struct_0(B) & l1_pre_topc(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( v3_tops_2(C,A,B) => v3_tops_2(k2_tops_2(A,B,C),B,A) ) ) ) ) ), file(tops_2,t70_tops_2), [interesting(0.00)]). fof(t56_topreala,theorem,( v3_tops_2(k2_topreala,k6_borsuk_1(k3_topalg_2,k3_topalg_2),k15_euclid(2)) ), file(topreala,t56_topreala), [interesting(0.00)]). fof(t25_topgrp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l1_pre_topc(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( v3_tops_2(C,A,B) <=> ( k1_relat_1(C) = k2_pre_topc(A) & k2_relat_1(C) = k2_pre_topc(B) & v2_funct_1(C) & ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( v3_pre_topc(D,A) <=> v3_pre_topc(k4_pre_topc(A,B,C,D),B) ) ) ) ) ) ) ) ), file(topgrp_1,t25_topgrp_1), [interesting(0.00)]). fof(t46_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(k2_relat_1(A),k1_relat_1(B)) => k1_relat_1(k5_relat_1(A,B)) = k1_relat_1(A) ) ) ) ), file(relat_1,t46_relat_1), [interesting(0.00)]). fof(d5_tops_2,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( l1_pre_topc(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( v3_tops_2(C,A,B) <=> ( k1_relat_1(C) = k2_pre_topc(A) & k2_relat_1(C) = k2_pre_topc(B) & v2_funct_1(C) & v5_pre_topc(C,A,B) & v5_pre_topc(k2_tops_2(A,B,C),B,A) ) ) ) ) ) ), file(tops_2,d5_tops_2), [interesting(0.00)]). fof(t55_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ! [C] : ( v1_relat_1(C) => k5_relat_1(k5_relat_1(A,B),C) = k5_relat_1(A,k5_relat_1(B,C)) ) ) ) ), file(relat_1,t55_relat_1), [interesting(0.00)]). fof(t65_tops_2,theorem,( ! [A] : ( l1_struct_0(A) => ! [B] : ( l1_struct_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( ( k2_relat_1(C) = k2_pre_topc(B) & v2_funct_1(C) ) => ( k5_relat_1(C,k2_tops_2(A,B,C)) = k6_relat_1(k1_relat_1(C)) & k5_relat_1(k2_tops_2(A,B,C),C) = k6_relat_1(k2_relat_1(C)) ) ) ) ) ) ), file(tops_2,t65_tops_2), [interesting(0.00)]). fof(t23_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k5_relat_1(B,C),A) = k1_funct_1(C,k1_funct_1(B,A)) ) ) ) ), file(funct_1,t23_funct_1), [interesting(0.00)]). fof(t35_funct_1,theorem,( ! [A,B] : ( r2_hidden(B,A) => k1_funct_1(k6_relat_1(A),B) = B ) ), file(funct_1,t35_funct_1), [interesting(0.00)]). fof(t43_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( B != k1_xboole_0 => ! [E] : ( ? [F] : ( r2_hidden(F,A) & r2_hidden(F,C) & E = k1_funct_1(D,F) ) => r2_hidden(E,k9_relat_1(D,C)) ) ) ) ), file(funct_2,t43_funct_2), [interesting(0.00)]). fof(t45_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ( v3_pre_topc(C,k6_borsuk_1(A,B)) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) & C = k5_setfam_1(u1_struct_0(k6_borsuk_1(A,B)),D) & ! [E] : ~ ( r2_hidden(E,D) & ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(B))) => ~ ( E = k12_mcart_1(u1_struct_0(A),u1_struct_0(B),F,G) & v3_pre_topc(F,A) & v3_pre_topc(G,B) ) ) ) ) ) ) ) ) ) ), file(borsuk_1,t45_borsuk_1), [interesting(0.00)]). fof(d4_tarski,definition,( ! [A,B] : ( B = k3_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(C,D) & r2_hidden(D,A) ) ) ) ), file(tarski,d4_tarski), [interesting(0.00)]). fof(t17_xboole_1,theorem,( ! [A,B] : r1_tarski(k3_xboole_0(A,B),A) ), file(xboole_1,t17_xboole_1), [interesting(0.00)]). fof(t38_tops_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(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))) => ( ( v3_pre_topc(B,A) & v3_pre_topc(C,A) ) => v3_pre_topc(k5_subset_1(u1_struct_0(A),B,C),A) ) ) ) ) ), file(tops_1,t38_tops_1), [interesting(0.00)]). fof(d4_tops_2,definition,( ! [A] : ( l1_struct_0(A) => ! [B] : ( l1_struct_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( ( k2_relat_1(C) = k2_pre_topc(B) & v2_funct_1(C) ) => k2_tops_2(A,B,C) = k2_funct_1(C) ) ) ) ) ), file(tops_2,d4_tops_2), [interesting(0.00)]). fof(t62_tops_2,theorem,( ! [A] : ( l1_struct_0(A) => ! [B] : ( ( ~ v3_struct_0(B) & l1_struct_0(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( ( k2_relat_1(C) = k2_pre_topc(B) & v2_funct_1(C) ) => ( k1_relat_1(k2_tops_2(A,B,C)) = k2_pre_topc(B) & k2_relat_1(k2_tops_2(A,B,C)) = k2_pre_topc(A) ) ) ) ) ) ), file(tops_2,t62_tops_2), [interesting(0.00)]). fof(t92_zfmisc_1,theorem,( ! [A,B] : ( r2_hidden(A,B) => r1_tarski(A,k3_tarski(B)) ) ), file(zfmisc_1,t92_zfmisc_1), [interesting(0.00)]). fof(t156_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r1_tarski(A,B) => r1_tarski(k9_relat_1(C,A),k9_relat_1(C,B)) ) ) ), file(relat_1,t156_relat_1), [interesting(0.00)]). fof(t1_partfun3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v2_funct_1(A) & r1_tarski(B,k1_relat_1(k2_funct_1(A))) ) => k9_relat_1(A,k9_relat_1(k2_funct_1(A),B)) = B ) ) ), file(partfun3,t1_partfun3), [interesting(0.00)]). fof(t29_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( k5_toprns_1(A,k20_euclid(A,B,C)) = 0 <=> B = C ) ) ) ) ), file(toprns_1,t29_toprns_1), [interesting(0.00)]). fof(d3_abian,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_abian(A,B) <=> ( r2_hidden(A,k1_relat_1(B)) & A = k1_funct_1(B,A) ) ) ) ), file(abian,d3_abian), [interesting(0.00)]). fof(t1_brouwer,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( r2_hidden(C,k1_brouwer(A,B)) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & C = k8_borsuk_1(A,B,D,E) & D != E ) ) ) ) ) ), file(brouwer,t1_brouwer), [interesting(0.00)]). fof(t25_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => u1_struct_0(k15_euclid(A)) = k1_euclid(A) ) ), file(euclid,t25_euclid), [interesting(0.00)]). fof(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(t37_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(A))) => ! [G] : ( m2_finseq_2(G,k1_numbers,k1_euclid(A)) => ! [H] : ( m2_finseq_2(H,k1_numbers,k1_euclid(A)) => ! [I] : ( m2_finseq_2(I,k1_numbers,k1_euclid(A)) => ~ ( G = D & H = E & I = F & D != E & r2_hidden(D,k1_topreal9(A,F,B)) & C = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,D),k20_euclid(A,D,F)))),k8_square_1(k1_quin_1(k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))),k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,D),k20_euclid(A,D,F))),k6_xcmplx_0(k15_rvsum_1(k11_euclid(A,k8_euclid(A,G,I))),k5_square_1(B))))),k4_real_1(2,k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))))) & ! [J] : ( m1_subset_1(J,u1_struct_0(k15_euclid(A))) => ~ ( k1_struct_0(k15_euclid(A),J) = k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,D,E),k3_topreal9(A,F,B)) & J = k17_euclid(A,k18_euclid(k6_xcmplx_0(1,C),A,D),k18_euclid(C,A,E)) ) ) ) ) ) ) ) ) ) ) ) ) ), file(topreal9,t37_topreal9), [interesting(0.00)]). fof(t38_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(A))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(A))) => ! [G] : ( m2_finseq_2(G,k1_numbers,k1_euclid(A)) => ! [H] : ( m2_finseq_2(H,k1_numbers,k1_euclid(A)) => ! [I] : ( m2_finseq_2(I,k1_numbers,k1_euclid(A)) => ~ ( G = k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E)) & H = E & I = F & D != E & r2_hidden(D,k3_topreal9(A,F,B)) & r2_hidden(E,k2_topreal9(A,F,B)) & ! [J] : ( m1_subset_1(J,u1_struct_0(k15_euclid(A))) => ~ ( J != D & k2_struct_0(k15_euclid(A),D,J) = k5_subset_1(u1_struct_0(k15_euclid(A)),k4_topreal9(A,D,E),k3_topreal9(A,F,B)) & ( r2_hidden(E,k3_topreal9(A,F,B)) => J = E ) & ( C = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E))),k20_euclid(A,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E)),F)))),k8_square_1(k1_quin_1(k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))),k3_xcmplx_0(2,k2_euclid_2(A,k20_euclid(A,E,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E))),k20_euclid(A,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E)),F))),k6_xcmplx_0(k15_rvsum_1(k11_euclid(A,k8_euclid(A,G,I))),k5_square_1(B))))),k4_real_1(2,k15_rvsum_1(k11_euclid(A,k8_euclid(A,H,G))))) => ( r2_hidden(E,k3_topreal9(A,F,B)) | J = k17_euclid(A,k18_euclid(k6_xcmplx_0(1,C),A,k17_euclid(A,k18_euclid(k6_real_1(1,2),A,D),k18_euclid(k6_real_1(1,2),A,E))),k18_euclid(C,A,E)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(topreal9,t38_topreal9), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(t19_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k1_euclid(A)) => ! [C] : ( m2_finseq_2(C,k1_numbers,k1_euclid(A)) => ( k12_euclid(k8_euclid(A,B,C)) = 0 <=> B = C ) ) ) ) ), file(euclid,t19_euclid), [interesting(0.00)]). fof(t116_rvsum_1,theorem,( ! [A] : ( m2_finseq_1(A,k1_numbers) => r1_xreal_0(0,k15_rvsum_1(k11_rvsum_1(A))) ) ), file(rvsum_1,t116_rvsum_1), [interesting(0.00)]). fof(d5_euclid,definition,( ! [A] : ( m2_finseq_1(A,k1_numbers) => k12_euclid(A) = k9_square_1(k15_rvsum_1(k11_rvsum_1(A))) ) ), file(euclid,d5_euclid), [interesting(0.00)]). fof(t82_square_1,theorem,( k9_square_1(0) = 0 ), file(square_1,t82_square_1), [interesting(0.00)]). fof(t12_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k1_euclid(A)) => r1_xreal_0(0,k12_euclid(B)) ) ) ), file(euclid,t12_euclid), [interesting(0.00)]). fof(d13_euclid,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => ( D = k20_euclid(A,B,C) <=> ! [E] : ( m2_finseq_2(E,k1_numbers,k1_euclid(A)) => ! [F] : ( m2_finseq_2(F,k1_numbers,k1_euclid(A)) => ( ( E = B & F = C ) => D = k8_euclid(A,E,F) ) ) ) ) ) ) ) ) ), file(euclid,d13_euclid), [interesting(0.00)]). fof(d6_toprns_1,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( C = k5_toprns_1(A,B) <=> ? [D] : ( m2_finseq_1(D,k1_numbers) & B = D & C = k12_euclid(D) ) ) ) ) ) ), file(toprns_1,d6_toprns_1), [interesting(0.00)]). fof(t106_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ ( r1_xreal_0(0,k2_xcmplx_0(A,k4_xcmplx_0(B))) & r1_xreal_0(k6_xcmplx_0(B,A),0) & r1_xreal_0(k2_xcmplx_0(k4_xcmplx_0(A),B),0) & r1_xreal_0(k2_xcmplx_0(B,k4_xcmplx_0(C)),k6_xcmplx_0(A,C)) & r1_xreal_0(k6_xcmplx_0(B,C),k2_xcmplx_0(A,k4_xcmplx_0(C))) & r1_xreal_0(k6_xcmplx_0(C,A),k6_xcmplx_0(C,B)) ) & r1_xreal_0(B,A) ) ) ) ) ), file(real_2,t106_real_2), [interesting(0.00)]). fof(t8_toprns_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k4_real_1(k18_complex1(B),k5_toprns_1(A,C)) = k5_toprns_1(A,k18_euclid(B,A,C)) ) ) ) ), file(toprns_1,t8_toprns_1), [interesting(0.00)]). fof(t161_complex1,theorem,( ! [A] : ( v1_xreal_0(A) => k7_square_1(k17_complex1(A)) = k5_square_1(A) ) ), file(complex1,t161_complex1), [interesting(0.00)]). fof(t51_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k20_euclid(A,B,k20_euclid(A,C,D)) = k17_euclid(A,k20_euclid(A,B,C),D) ) ) ) ) ), file(euclid,t51_euclid), [interesting(0.00)]). fof(t1_topreal9,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(A))) => k20_euclid(A,k20_euclid(A,B,C),D) = k20_euclid(A,k20_euclid(A,B,D),C) ) ) ) ) ), file(topreal9,t1_topreal9), [interesting(0.00)]). fof(t45_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k20_euclid(A,B,C) = k17_euclid(A,B,k19_euclid(A,C)) ) ) ) ), file(euclid,t45_euclid), [interesting(0.00)]). fof(t44_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( v1_xreal_0(C) => ( k19_euclid(A,k18_euclid(C,A,B)) = k18_euclid(k4_xcmplx_0(C),A,B) & k19_euclid(A,k18_euclid(C,A,B)) = k18_euclid(C,A,k19_euclid(A,B)) ) ) ) ) ), file(euclid,t44_euclid), [interesting(0.00)]). fof(t48_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ( k19_euclid(A,k20_euclid(A,B,C)) = k20_euclid(A,C,B) & k19_euclid(A,k20_euclid(A,B,C)) = k17_euclid(A,k19_euclid(A,B),C) ) ) ) ) ), file(euclid,t48_euclid), [interesting(0.00)]). fof(t67_euclid_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => k7_square_1(k5_toprns_1(A,k17_euclid(A,B,C))) = k2_xcmplx_0(k2_xcmplx_0(k7_square_1(k5_toprns_1(A,B)),k3_xcmplx_0(2,k2_euclid_2(A,C,B))),k7_square_1(k5_toprns_1(A,C))) ) ) ) ), file(euclid_2,t67_euclid_2), [interesting(0.00)]). fof(t41_euclid_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,u1_struct_0(k15_euclid(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k15_euclid(A))) => ! [D] : ( v1_xreal_0(D) => k2_euclid_2(A,k18_euclid(D,A,B),C) = k3_xcmplx_0(D,k2_euclid_2(A,B,C)) ) ) ) ) ), file(euclid_2,t41_euclid_2), [interesting(0.00)]). fof(t7_brouwer,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( ( v1_xreal_0(B) & ~ v3_xreal_0(B) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m2_subset_1(C,k1_numbers,k5_numbers) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(k15_euclid(C))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k15_euclid(C))) => ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(C))) => ! [G] : ( m1_subset_1(G,k1_euclid(C)) => ! [H] : ( m1_subset_1(H,k1_euclid(C)) => ! [I] : ( m1_subset_1(I,k1_euclid(C)) => ( ( G = D & H = E & I = F & m1_subset_1(D,u1_struct_0(k2_brouwer(C,F,B))) & m1_subset_1(E,u1_struct_0(k2_brouwer(C,F,B))) & A = k7_xcmplx_0(k2_xcmplx_0(k4_xcmplx_0(k2_euclid_2(C,k20_euclid(C,E,D),k20_euclid(C,D,F))),k8_square_1(k6_xcmplx_0(k5_square_1(k2_euclid_2(C,k20_euclid(C,E,D),k20_euclid(C,D,F))),k3_xcmplx_0(k15_rvsum_1(k11_rvsum_1(k8_euclid(C,H,G))),k6_xcmplx_0(k15_rvsum_1(k11_rvsum_1(k8_euclid(C,G,I))),k5_square_1(B)))))),k15_rvsum_1(k11_rvsum_1(k8_euclid(C,H,G)))) ) => ( D = E | k3_brouwer(C,F,D,E,B) = k17_euclid(C,k18_euclid(k6_xcmplx_0(1,A),C,D),k18_euclid(A,C,E)) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_brouwer,d3_xboole_0,t26_topreal9,t54_euclid,t33_euclid,t9_jordan2c,t49_euclid,t53_euclid,t19_euclid,t116_rvsum_1,d5_euclid,t82_square_1,d1_quin_1,t3_brouwer,t8_topreal9,d5_euclid,t12_euclid,d13_euclid,d6_toprns_1,d5_euclid,t116_rvsum_1,d4_square_1,t116_rvsum_1,d4_square_1,d13_euclid,d6_toprns_1,t77_square_1,t106_real_2,d1_quin_1,t131_xreal_1,t133_xreal_1,t174_real_2,d1_xreal_0,t8_toprns_1,t161_complex1,d3_xboole_0,t9_topreal9,t54_euclid,t33_euclid,t51_euclid,t1_topreal9,t53_euclid,t45_euclid,t44_euclid,t48_euclid,t67_euclid_2,t41_euclid_2,d2_polyeq_1,t133_xreal_1,t26_xreal_1,t9_xreal_1,t97_square_1,t85_square_1,t92_xcmplx_1,t5_polyeq_1,d2_polyeq_1,t16_quin_1,d3_polyeq_1,t11_polyeq_1,t131_xreal_1,t73_real_1,t11_xreal_1,t8_xreal_1,d4_square_1,t9_xreal_1,t128_real_2,t135_xreal_1,t33_euclid,t31_euclid,d3_brouwer,t134_xreal_1,t89_square_1,t128_real_2,t90_square_1,t106_real_2]), [file(brouwer,t7_brouwer),interesting(0.00)]).