fof(t92_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,B,B) ) => ( r1_borsuk_6(A,B,C) => r3_borsuk_2(A,B,B,k1_borsuk_2(A,B,C,B,D,k2_borsuk_2(A,B,C,D)),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_borsuk_2,t39_yellow12,t40_yellow12,d2_borsuk_2,t12_jgraph_3,t10_topmetr,t1_jordan1,d5_borsuk_1,t23_mcart_1,t106_zfmisc_1,d5_funct_3,d1_funct_2,t67_borsuk_6,t72_funct_1,t23_funct_1,d5_borsuk_2,t58_tops_2,t12_jgraph_3,t10_topmetr,t1_jordan1,d5_borsuk_1,t23_mcart_1,t106_zfmisc_1,d6_funct_3,d1_funct_2,t72_funct_1,t23_funct_1,d6_borsuk_2,t12_jgraph_3,t10_topmetr,t1_jordan1,d5_borsuk_1,t23_mcart_1,t106_zfmisc_1,d5_funct_3,d1_funct_2,t68_borsuk_6,t72_funct_1,t23_funct_1,d5_borsuk_2,t15_xboole_1,t1_jordan1,d1_struct_0,t1_jordan1,d3_pre_topc,d10_pre_topc,d10_pre_topc,t7_xboole_1,d10_pre_topc,d10_pre_topc,d10_pre_topc,t65_borsuk_6,d3_xboole_0,t1_jordan1,t1_jordan1,t7_xboole_1,t6_jordan16,t7_xboole_1,t6_jordan16,t34_tops_2,t34_tops_2,t9_jgraph_2,d10_pre_topc,d10_pre_topc,d10_pre_topc,t64_borsuk_6,t83_borsuk_1,d5_borsuk_1,d3_pre_topc,t80_borsuk_6,t23_xboole_1,t74_borsuk_6,t75_borsuk_6,d3_xboole_0,t37_zfmisc_1,t12_xboole_1,t66_borsuk_6,d3_xboole_0,t1_jordan1,t1_jordan1,t31_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d6_borsuk_2,t36_tops_1,d10_pre_topc,t9_jgraph_2,t7_mcart_1,t78_borsuk_6,t79_borsuk_6,t1_jordan1,d1_funct_2,t1_jordan1,t79_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,t12_funct_4,d5_borsuk_2,t74_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,d2_borsuk_2,d5_borsuk_2,t77_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d5_borsuk_2,d5_real_1,t7_mcart_1,d1_funct_2,t2_jordan5a,t71_borsuk_6,t1_jordan1,d1_funct_2,t73_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,t14_funct_4,d2_borsuk_2,d2_borsuk_2,d5_seqm_3,t74_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,d2_borsuk_2,d5_seqm_3,t2_jordan5a,l94_borsuk_6,t69_borsuk_6,t1_jordan1,t7_mcart_1,t68_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,t70_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,d2_borsuk_2,t72_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,t2_jordan5a,l94_borsuk_6,t76_borsuk_6,t7_mcart_1,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,d7_borsuk_2]), [file(borsuk_6,t92_borsuk_6),interesting(1.00)]). fof(t94_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,C,C) ) => ( r1_borsuk_6(A,B,C) => r3_borsuk_2(A,C,C,k1_borsuk_2(A,C,B,C,k2_borsuk_2(A,B,C,D),D),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_borsuk_2,t39_yellow12,t40_yellow12,d2_borsuk_2,t12_jgraph_3,t10_topmetr,t1_jordan1,d5_borsuk_1,t23_mcart_1,t106_zfmisc_1,d5_funct_3,d1_funct_2,t67_borsuk_6,t72_funct_1,t23_funct_1,d5_borsuk_2,t58_tops_2,t12_jgraph_3,t10_topmetr,t1_jordan1,d5_borsuk_1,t23_mcart_1,t106_zfmisc_1,d6_funct_3,t4_jordan5b,d1_funct_2,t72_funct_1,t23_funct_1,d6_borsuk_2,t12_jgraph_3,t10_topmetr,t1_jordan1,d5_borsuk_1,t23_mcart_1,t106_zfmisc_1,d5_funct_3,d1_funct_2,t68_borsuk_6,t72_funct_1,t23_funct_1,d5_borsuk_2,t15_xboole_1,t1_jordan1,d1_struct_0,t1_jordan1,d3_pre_topc,d10_pre_topc,d10_pre_topc,t7_xboole_1,d10_pre_topc,d10_pre_topc,d10_pre_topc,t65_borsuk_6,d3_xboole_0,t1_jordan1,t1_jordan1,t7_xboole_1,t6_jordan16,t7_xboole_1,t6_jordan16,t34_tops_2,t34_tops_2,t9_jgraph_2,d10_pre_topc,d10_pre_topc,t64_borsuk_6,t83_borsuk_1,d5_borsuk_1,d3_pre_topc,t80_borsuk_6,t23_xboole_1,t74_borsuk_6,t75_borsuk_6,d3_xboole_0,t37_zfmisc_1,t12_xboole_1,t66_borsuk_6,d3_xboole_0,t1_jordan1,t1_jordan1,t31_borsuk_6,t4_jordan5b,t1_jordan1,d1_funct_2,t14_funct_4,d6_borsuk_2,t36_tops_1,d10_pre_topc,t9_jgraph_2,t7_mcart_1,t78_borsuk_6,t79_borsuk_6,t1_jordan1,d1_funct_2,t1_jordan1,t79_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,t12_funct_4,d5_borsuk_2,t74_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,d2_borsuk_2,d5_borsuk_2,t77_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d5_borsuk_2,d5_real_1,t7_mcart_1,d1_funct_2,t2_jordan5a,t71_borsuk_6,t1_jordan1,d1_funct_2,t73_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,t14_funct_4,d2_borsuk_2,d2_borsuk_2,d5_seqm_3,t74_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,d2_borsuk_2,d5_seqm_3,t2_jordan5a,l94_borsuk_6,t69_borsuk_6,t1_jordan1,t7_mcart_1,t68_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,t70_borsuk_6,t1_jordan1,d1_funct_2,t12_funct_4,d2_borsuk_2,t72_borsuk_6,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,t2_jordan5a,l94_borsuk_6,t76_borsuk_6,t7_mcart_1,t1_jordan1,d1_funct_2,t14_funct_4,d2_borsuk_2,d7_borsuk_2]), [file(borsuk_6,t94_borsuk_6),interesting(1.00)]). fof(t62_borsuk_6,theorem,( k7_borsuk_6 = a_0_13_borsuk_6 ), inference(mizar_proof,[status(thm)],[t29_borsuk_6,d3_tarski,d11_borsuk_6,t7_mcart_1,d10_xboole_0,d3_tarski,d5_borsuk_1,t23_mcart_1,t31_borsuk_6,t31_borsuk_6,d11_borsuk_6]), [file(borsuk_6,t62_borsuk_6),interesting(0.97)]). fof(t63_borsuk_6,theorem,( k8_borsuk_6 = a_0_14_borsuk_6 ), inference(mizar_proof,[status(thm)],[t30_borsuk_6,d3_tarski,d12_borsuk_6,t7_mcart_1,d10_xboole_0,d3_tarski,d5_borsuk_1,t23_mcart_1,t31_borsuk_6,t31_borsuk_6,d12_borsuk_6]), [file(borsuk_6,t63_borsuk_6),interesting(0.96)]). fof(t93_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,B,B) ) => r4_borsuk_2(A,B,B,k1_borsuk_2(A,B,C,B,D,k2_borsuk_2(A,B,C,D)),E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t92_borsuk_6]), [file(borsuk_6,t93_borsuk_6),interesting(0.96)]). fof(t95_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,C,C) ) => r4_borsuk_2(A,C,C,k1_borsuk_2(A,C,B,C,k2_borsuk_2(A,B,C,D),D),E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t94_borsuk_6]), [file(borsuk_6,t95_borsuk_6),interesting(0.96)]). fof(t61_borsuk_6,theorem,( k6_borsuk_6 = a_0_12_borsuk_6 ), inference(mizar_proof,[status(thm)],[t28_borsuk_6,d3_tarski,d10_borsuk_6,t7_mcart_1,d10_xboole_0,d3_tarski,d5_borsuk_1,t23_mcart_1,t31_borsuk_6,t31_borsuk_6,d10_borsuk_6]), [file(borsuk_6,t61_borsuk_6),interesting(0.95)]). fof(t65_borsuk_6,theorem,( k5_subset_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),k6_borsuk_6,k7_borsuk_6) = a_0_15_borsuk_6 ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,t61_borsuk_6,t62_borsuk_6,t1_xreal_1,d10_xboole_0,d3_tarski,d5_borsuk_1,t23_mcart_1,t10_mcart_1,d10_borsuk_6,t2_jordan5a,t21_xreal_1,t73_real_1,t219_xreal_1,t220_xreal_1,d11_borsuk_6,d3_xboole_0]), [file(borsuk_6,t65_borsuk_6),interesting(0.85)]). fof(t66_borsuk_6,theorem,( k5_subset_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),k8_borsuk_6,k7_borsuk_6) = a_0_16_borsuk_6 ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,t63_borsuk_6,t62_borsuk_6,t1_xreal_1,d10_xboole_0,d3_tarski,d5_borsuk_1,t23_mcart_1,t10_mcart_1,d12_borsuk_6,t2_jordan5a,t21_xreal_1,t73_real_1,t221_xreal_1,t222_xreal_1,d11_borsuk_6,d3_xboole_0]), [file(borsuk_6,t66_borsuk_6),interesting(0.85)]). fof(t88_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,C,C) ) => ( r1_borsuk_6(A,B,C) => r3_borsuk_2(A,B,C,k1_borsuk_2(A,B,C,C,D,E),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t58_borsuk_6,t53_borsuk_6,t55_borsuk_6]), [file(borsuk_6,t88_borsuk_6),interesting(0.82)]). fof(t90_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,B,B) ) => ( r1_borsuk_6(A,B,C) => r3_borsuk_2(A,B,C,k1_borsuk_2(A,B,B,C,E,D),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t59_borsuk_6,t53_borsuk_6,t56_borsuk_6]), [file(borsuk_6,t90_borsuk_6),interesting(0.82)]). fof(t8_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => m1_subset_1(k3_xcmplx_0(A,B),u1_struct_0(k5_topmetr)) ) ) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t121_real_2,t140_real_2,t2_jordan5a]), [file(borsuk_6,t8_borsuk_6),interesting(0.75)]). fof(t89_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,C,C) ) => r4_borsuk_2(A,B,C,k1_borsuk_2(A,B,C,C,D,E),D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t88_borsuk_6]), [file(borsuk_6,t89_borsuk_6),interesting(0.75)]). fof(t91_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,B,B) ) => r4_borsuk_2(A,B,C,k1_borsuk_2(A,B,B,C,E,D),D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t90_borsuk_6]), [file(borsuk_6,t91_borsuk_6),interesting(0.75)]). fof(t71_borsuk_6,theorem,( ! [A] : ( r2_hidden(k4_tarski(A,1),k8_borsuk_6) => A = 1 ) ), inference(mizar_proof,[status(thm)],[d12_borsuk_6,t2_jordan5a,t33_zfmisc_1,t21_xreal_1,t73_real_1,t1_xreal_1]), [file(borsuk_6,t71_borsuk_6),interesting(0.75)]). fof(t72_borsuk_6,theorem,( r2_hidden(k4_tarski(0,1),k7_borsuk_6) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,d11_borsuk_6]), [file(borsuk_6,t72_borsuk_6),interesting(0.74)]). fof(t23_borsuk_6,theorem, ( v4_pre_topc(a_0_8_borsuk_6,k15_euclid(2)) & m1_subset_1(a_0_8_borsuk_6,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), inference(mizar_proof,[status(thm)],[t22_borsuk_6,t20_borsuk_6,s10_domain_1,t35_tops_1]), [file(borsuk_6,t23_borsuk_6),interesting(0.73)]). fof(t27_borsuk_6,theorem, ( v4_pre_topc(a_0_11_borsuk_6,k6_borsuk_1(k3_topmetr,k3_topmetr)) & m1_subset_1(a_0_11_borsuk_6,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k3_topmetr,k3_topmetr)))) ), inference(mizar_proof,[status(thm)],[s7_domain_1,s7_domain_1,t24_borsuk_6,t85_topreal6,d3_tarski,d12_funct_1,d5_borsuk_1,d2_zfmisc_1,t24_topmetr,d16_euclid,d14_euclid,t61_finseq_1,d15_euclid,t61_finseq_1,t7_mcart_1,d10_xboole_0,d3_tarski,t55_euclid,d16_euclid,t56_euclid,t56_euclid,t24_topmetr,t106_zfmisc_1,d5_borsuk_1,d5_borsuk_1,t7_mcart_1,d1_funct_2,d12_funct_1,t23_borsuk_6,t72_tops_2]), [file(borsuk_6,t27_borsuk_6),interesting(0.73)]). fof(t73_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => r2_hidden(k4_tarski(A,1),k7_borsuk_6) ) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t2_jordan5a,t66_xreal_1,t92_real_1,t66_xreal_1,t92_real_1,d11_borsuk_6]), [file(borsuk_6,t73_borsuk_6),interesting(0.73)]). fof(t70_borsuk_6,theorem,( ! [A] : ( r2_hidden(k4_tarski(0,A),k7_borsuk_6) => A = 1 ) ), inference(mizar_proof,[status(thm)],[d11_borsuk_6,t2_jordan5a,t33_zfmisc_1,t1_xreal_1]), [file(borsuk_6,t70_borsuk_6),interesting(0.73)]). fof(t21_borsuk_6,theorem, ( v4_pre_topc(a_0_6_borsuk_6,k15_euclid(2)) & m1_subset_1(a_0_6_borsuk_6,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), inference(mizar_proof,[status(thm)],[s1_jgraph_2,t57_jgraph_2,d1_funct_2,t54_jgraph_2,t17_borsuk_6,t1_msafree3,d12_pre_topc]), [file(borsuk_6,t21_borsuk_6),interesting(0.72)]). fof(t25_borsuk_6,theorem, ( v4_pre_topc(a_0_9_borsuk_6,k6_borsuk_1(k3_topmetr,k3_topmetr)) & m1_subset_1(a_0_9_borsuk_6,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k3_topmetr,k3_topmetr)))) ), inference(mizar_proof,[status(thm)],[s7_domain_1,s7_domain_1,t24_borsuk_6,t85_topreal6,d3_tarski,d12_funct_1,d5_borsuk_1,d2_zfmisc_1,t24_topmetr,d16_euclid,d14_euclid,t61_finseq_1,d15_euclid,t61_finseq_1,t7_mcart_1,d10_xboole_0,d3_tarski,t55_euclid,d16_euclid,t56_euclid,t56_euclid,t106_zfmisc_1,d5_borsuk_1,t24_topmetr,d5_borsuk_1,t24_topmetr,t7_mcart_1,d1_funct_2,d12_funct_1,t21_borsuk_6,t72_tops_2]), [file(borsuk_6,t25_borsuk_6),interesting(0.72)]). fof(t22_borsuk_6,theorem, ( v4_pre_topc(a_0_4_borsuk_6,k15_euclid(2)) & m1_subset_1(a_0_4_borsuk_6,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), inference(mizar_proof,[status(thm)],[s1_jgraph_2,t57_jgraph_2,d1_funct_2,t54_jgraph_2,t16_borsuk_6,t1_msafree3,d12_pre_topc]), [file(borsuk_6,t22_borsuk_6),interesting(0.72)]). fof(t20_borsuk_6,theorem, ( v4_pre_topc(a_0_2_borsuk_6,k15_euclid(2)) & m1_subset_1(a_0_2_borsuk_6,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), inference(mizar_proof,[status(thm)],[s1_jgraph_2,t56_jgraph_2,d1_funct_2,t54_jgraph_2,t15_borsuk_6,t1_msafree3,d12_pre_topc]), [file(borsuk_6,t20_borsuk_6),interesting(0.72)]). fof(t19_borsuk_6,theorem, ( v4_pre_topc(a_0_0_borsuk_6,k15_euclid(2)) & m1_subset_1(a_0_0_borsuk_6,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), inference(mizar_proof,[status(thm)],[s1_jgraph_2,t56_jgraph_2,d1_funct_2,t54_jgraph_2,t14_borsuk_6,t1_msafree3,d12_pre_topc]), [file(borsuk_6,t19_borsuk_6),interesting(0.72)]). fof(t26_borsuk_6,theorem, ( v4_pre_topc(a_0_10_borsuk_6,k6_borsuk_1(k3_topmetr,k3_topmetr)) & m1_subset_1(a_0_10_borsuk_6,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k3_topmetr,k3_topmetr)))) ), inference(mizar_proof,[status(thm)],[s7_domain_1,s7_domain_1,t24_borsuk_6,t85_topreal6,d3_tarski,d12_funct_1,d5_borsuk_1,d2_zfmisc_1,t24_topmetr,d16_euclid,d14_euclid,t61_finseq_1,d15_euclid,t61_finseq_1,t7_mcart_1,d10_xboole_0,d3_tarski,t55_euclid,d16_euclid,t56_euclid,t56_euclid,t24_topmetr,t106_zfmisc_1,d5_borsuk_1,d5_borsuk_1,t7_mcart_1,d1_funct_2,d12_funct_1,t19_borsuk_6,t72_tops_2]), [file(borsuk_6,t26_borsuk_6),interesting(0.72)]). fof(t29_borsuk_6,theorem, ( ~ v1_xboole_0(a_0_13_borsuk_6) & v4_pre_topc(a_0_13_borsuk_6,k6_borsuk_1(k5_topmetr,k5_topmetr)) & m1_subset_1(a_0_13_borsuk_6,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t106_zfmisc_1,d5_borsuk_1,t7_mcart_1,t27_borsuk_6,t25_borsuk_3,d3_tarski,t35_borsuk_1,d3_pre_topc,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,t17_xboole_1,d3_pre_topc,t43_pre_topc]), [file(borsuk_6,t29_borsuk_6),interesting(0.71)]). fof(t12_borsuk_6,theorem,( m1_borsuk_2(k7_grcat_1(k5_topmetr),k22_borsuk_1,k23_borsuk_1,k24_borsuk_1) ), inference(mizar_proof,[status(thm)],[d17_borsuk_1,d18_borsuk_1,t91_tmap_1,d4_borsuk_2]), [file(borsuk_6,t12_borsuk_6),interesting(0.70)]). fof(t55_borsuk_6,theorem, ( k1_funct_1(k3_borsuk_6,0) = 0 & k1_funct_1(k3_borsuk_6,1) = 1 ), inference(mizar_proof,[status(thm)],[t2_jordan5a,d7_borsuk_6,d7_borsuk_6]), [file(borsuk_6,t55_borsuk_6),interesting(0.70)]). fof(t56_borsuk_6,theorem, ( k1_funct_1(k4_borsuk_6,0) = 0 & k1_funct_1(k4_borsuk_6,1) = 1 ), inference(mizar_proof,[status(thm)],[t2_jordan5a,d8_borsuk_6,d8_borsuk_6]), [file(borsuk_6,t56_borsuk_6),interesting(0.70)]). fof(t28_borsuk_6,theorem, ( ~ v1_xboole_0(a_0_12_borsuk_6) & v4_pre_topc(a_0_12_borsuk_6,k6_borsuk_1(k5_topmetr,k5_topmetr)) & m1_subset_1(a_0_12_borsuk_6,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t106_zfmisc_1,d5_borsuk_1,t7_mcart_1,t25_borsuk_6,t25_borsuk_3,d3_tarski,t35_borsuk_1,d3_pre_topc,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,t17_xboole_1,d3_pre_topc,t43_pre_topc]), [file(borsuk_6,t28_borsuk_6),interesting(0.70)]). fof(t30_borsuk_6,theorem, ( ~ v1_xboole_0(a_0_14_borsuk_6) & v4_pre_topc(a_0_14_borsuk_6,k6_borsuk_1(k5_topmetr,k5_topmetr)) & m1_subset_1(a_0_14_borsuk_6,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t106_zfmisc_1,d5_borsuk_1,t7_mcart_1,t26_borsuk_6,t25_borsuk_3,d3_tarski,t35_borsuk_1,d3_pre_topc,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,t17_xboole_1,d3_pre_topc,t43_pre_topc]), [file(borsuk_6,t30_borsuk_6),interesting(0.70)]). fof(t87_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( m1_borsuk_2(E,A,B,C) => ! [F] : ( m1_borsuk_2(F,A,B,C) => ( ( r3_borsuk_2(A,B,C,D,E) & r3_borsuk_2(A,B,C,E,F) ) => r3_borsuk_2(A,B,C,D,F) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_borsuk_2,d7_borsuk_2,t27_topmetr,t15_treal_1,t27_topmetr,t15_treal_1,d1_funct_2,d1_funct_2,t12_borsuk_2,t12_borsuk_2,t12_relset_1,t12_relset_1,t27_topmetr,t88_funct_3,t119_zfmisc_1,d1_funct_2,d5_borsuk_1,t46_relat_1,d9_funct_3,t25_topmetr,t83_borsuk_1,t83_borsuk_1,t1_treal_1,t83_borsuk_1,t119_zfmisc_1,t48_rcomp_1,t48_rcomp_1,d5_borsuk_1,t106_zfmisc_1,t83_borsuk_1,t1_treal_1,t83_borsuk_1,t119_zfmisc_1,t48_rcomp_1,d5_borsuk_1,t106_zfmisc_1,t48_rcomp_1,t83_borsuk_1,t48_rcomp_1,t1_treal_1,t48_rcomp_1,t25_topmetr,t83_borsuk_1,t48_rcomp_1,t1_treal_1,t83_borsuk_1,d3_pre_topc,t31_waybel34,t7_jgraph_5,t26_borsuk_3,t7_jgraph_5,t26_borsuk_3,d10_pre_topc,t120_zfmisc_1,t83_borsuk_1,t2_treal_1,d5_borsuk_1,t12_pre_topc,t58_tops_2,t58_tops_2,t2_jordan5a,t49_borsuk_4,t27_borsuk_3,t12_compts_1,t49_borsuk_4,t27_borsuk_3,t12_compts_1,t122_zfmisc_1,t1_topmetr2,d1_funct_2,d5_borsuk_1,d1_funct_2,d5_borsuk_1,d9_funct_3,d9_funct_3,t48_rcomp_1,t25_topmetr,d2_zfmisc_1,d1_tarski,d1_rcomp_1,t2_jordan5a,t2_jordan5a,t48_rcomp_1,t25_topmetr,d17_borsuk_1,d18_borsuk_1,t8_treal_1,t14_treal_1,t88_xcmplx_1,t90_xcmplx_1,d18_borsuk_1,t8_treal_1,t25_topmetr,t14_treal_1,d17_borsuk_1,d18_borsuk_1,t8_treal_1,t106_zfmisc_1,t106_zfmisc_1,t23_funct_1,t86_funct_3,t91_tmap_1,t91_tmap_1,t86_funct_3,t23_funct_1,t1_borsuk_2,t25_topmetr,t25_topmetr,t25_topmetr,t48_rcomp_1,t106_zfmisc_1,t48_rcomp_1,t106_zfmisc_1,d17_borsuk_1,d18_borsuk_1,t8_treal_1,t14_treal_1,d1_treal_1,t12_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,t48_rcomp_1,t106_zfmisc_1,t106_zfmisc_1,d2_treal_1,t16_treal_1,t14_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,t2_jordan5a,t2_jordan5a,t2_jordan5a,t48_rcomp_1,t106_zfmisc_1,t48_rcomp_1,t106_zfmisc_1,d17_borsuk_1,d18_borsuk_1,t8_treal_1,d1_xreal_0,t14_treal_1,d2_treal_1,d1_treal_1,d1_treal_1,t6_borsuk_6,t12_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,t48_rcomp_1,t106_zfmisc_1,t48_rcomp_1,t106_zfmisc_1,t14_treal_1,d2_treal_1,d1_treal_1,d1_treal_1,t6_borsuk_6,t12_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,t2_jordan5a,t2_jordan5a,t48_rcomp_1,t106_zfmisc_1,t106_zfmisc_1,d17_borsuk_1,d18_borsuk_1,t8_treal_1,d1_xreal_0,t14_treal_1,d2_treal_1,d1_treal_1,d1_treal_1,d2_treal_1,t7_borsuk_6,t14_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,t106_zfmisc_1,t106_zfmisc_1,t14_treal_1,d2_treal_1,d1_treal_1,d1_treal_1,d2_treal_1,t7_borsuk_6,t14_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,d7_borsuk_2]), [file(borsuk_6,t87_borsuk_6),interesting(0.69)]). fof(t75_borsuk_6,theorem,( r2_hidden(k4_tarski(k6_real_1(1,2),0),k7_borsuk_6) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,d11_borsuk_6]), [file(borsuk_6,t75_borsuk_6),interesting(0.68)]). fof(t85_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( m1_borsuk_2(E,A,B,C) => ( ( r1_borsuk_6(A,B,C) & r3_borsuk_2(A,B,C,D,E) ) => r3_borsuk_2(A,C,B,k2_borsuk_2(A,B,C,D),k2_borsuk_2(A,B,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_borsuk_2,t27_topmetr,t11_treal_1,t27_topmetr,t11_treal_1,t12_borsuk_2,d1_funct_2,t2_jordan5a,d7_borsuk_2,t58_tops_2,t27_topmetr,d1_treal_1,d2_treal_1,t10_treal_1,t2_jordan5a,d1_xreal_0,t4_jordan5b,d1_xreal_0,d9_funct_3,t91_tmap_1,t2_jordan5a,d9_funct_3,t91_tmap_1,d9_funct_3,t106_zfmisc_1,t106_zfmisc_1,t23_funct_1,d6_borsuk_2,t23_funct_1,d6_borsuk_2,t83_borsuk_1,t27_topmetr,d1_treal_1,d2_treal_1,t10_treal_1,t2_jordan5a,d1_funct_2,t2_jordan5a,d9_funct_3,t91_tmap_1,d9_funct_3,t91_tmap_1,t4_jordan5b,d9_funct_3,t106_zfmisc_1,t106_zfmisc_1,t23_funct_1,t23_funct_1]), [file(borsuk_6,t85_borsuk_6),interesting(0.67)]). fof(t69_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => r2_hidden(k4_tarski(0,A),k6_borsuk_6) ) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t2_jordan5a,d10_borsuk_6]), [file(borsuk_6,t69_borsuk_6),interesting(0.67)]). fof(t76_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => r2_hidden(k4_tarski(1,A),k8_borsuk_6) ) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t2_jordan5a,d12_borsuk_6]), [file(borsuk_6,t76_borsuk_6),interesting(0.67)]). fof(t80_borsuk_6,theorem,( k5_subset_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),k6_borsuk_6,k8_borsuk_6) = k1_tarski(k4_tarski(k6_real_1(1,2),0)) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d5_borsuk_1,t68_borsuk_6,t67_borsuk_6,t1_xreal_1,t63_borsuk_6,t31_borsuk_6,t2_jordan5a,t23_mcart_1,d1_tarski,d10_xboole_0,t2_jordan5a,t78_borsuk_6,t77_borsuk_6,d3_xboole_0,t37_zfmisc_1]), [file(borsuk_6,t80_borsuk_6),interesting(0.63)]). fof(t74_borsuk_6,theorem, ( r2_hidden(k4_tarski(k6_real_1(1,2),0),k8_borsuk_6) & r2_hidden(k4_tarski(1,1),k8_borsuk_6) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,d12_borsuk_6,d12_borsuk_6]), [file(borsuk_6,t74_borsuk_6),interesting(0.63)]). fof(t50_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ( r1_borsuk_6(A,B,C) => ! [D] : ( m1_borsuk_2(D,A,B,C) => D = k2_borsuk_2(A,C,B,k2_borsuk_2(A,B,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_jordan5b,d6_borsuk_2,d6_borsuk_2,t113_funct_2]), [file(borsuk_6,t50_borsuk_6),interesting(0.59)]). fof(t37_borsuk_6,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(D,C) & ~ ( k1_funct_1(k1_borsuk_6(A,B,C,D),A) = C & k1_funct_1(k1_borsuk_6(A,B,C,D),B) = D ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t48_rcomp_1,t25_topmetr,d1_funct_2,t23_funct_1,d1_treal_1,t16_treal_1,t12_treal_1,d1_treal_1,t48_rcomp_1,t25_topmetr,d1_funct_2,t23_funct_1,d2_treal_1,t16_treal_1,t12_treal_1,d2_treal_1]), [file(borsuk_6,t37_borsuk_6),interesting(0.59)]). fof(t46_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( r1_borsuk_6(A,B,C) & r1_borsuk_6(A,C,D) ) => r1_borsuk_6(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_borsuk_2,d2_borsuk_2,t27_jordan20]), [file(borsuk_6,t46_borsuk_6),interesting(0.58)]). fof(t57_borsuk_6,theorem, ( k1_funct_1(k5_borsuk_6,0) = 0 & k1_funct_1(k5_borsuk_6,1) = 1 ), inference(mizar_proof,[status(thm)],[t2_jordan5a,d9_borsuk_6,d9_borsuk_6]), [file(borsuk_6,t57_borsuk_6),interesting(0.58)]). fof(t58_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,C,C) ) => ( r1_borsuk_6(A,B,C) => k2_borsuk_6(A,B,C,D,k3_borsuk_6) = k1_borsuk_2(A,B,C,C,D,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t2_jordan5a,d1_funct_2,d6_borsuk_6,t55_borsuk_6,t23_funct_1,d7_borsuk_6,d5_borsuk_2,t7_borsuk_6,d1_funct_2,d7_borsuk_6,d2_borsuk_2,d2_borsuk_2,d5_seqm_3,d5_borsuk_2,t113_funct_2]), [file(borsuk_6,t58_borsuk_6),interesting(0.58)]). fof(t78_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ( r1_xreal_0(A,k6_real_1(1,2)) => r2_hidden(k4_tarski(A,0),k6_borsuk_6) ) ) ), inference(mizar_proof,[status(thm)],[t66_xreal_1,t92_real_1,t2_jordan5a,d10_borsuk_6]), [file(borsuk_6,t78_borsuk_6),interesting(0.58)]). fof(t77_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ( r1_xreal_0(k6_real_1(1,2),A) => r2_hidden(k4_tarski(A,0),k8_borsuk_6) ) ) ), inference(mizar_proof,[status(thm)],[t66_xreal_1,t92_real_1,t2_jordan5a,d12_borsuk_6]), [file(borsuk_6,t77_borsuk_6),interesting(0.58)]). fof(t59_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( ( v5_seqm_3(E) & m1_borsuk_2(E,A,B,B) ) => ( r1_borsuk_6(A,B,C) => k2_borsuk_6(A,B,C,D,k4_borsuk_6) = k1_borsuk_2(A,B,B,C,E,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t2_jordan5a,d1_funct_2,d6_borsuk_6,t56_borsuk_6,t23_funct_1,t6_borsuk_6,d1_funct_2,d8_borsuk_6,d2_borsuk_2,d2_borsuk_2,d5_seqm_3,d5_borsuk_2,d8_borsuk_6,d5_borsuk_2,t113_funct_2]), [file(borsuk_6,t59_borsuk_6),interesting(0.57)]). fof(t1_borsuk_6,theorem,( u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)) = k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(0,1),k1_rcomp_1(0,1)) ), inference(mizar_proof,[status(thm)],[t83_borsuk_1,d5_borsuk_1]), [file(borsuk_6,t1_borsuk_6),interesting(0.57)]). fof(t18_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ( v1_borsuk_6(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => v1_xreal_0(B) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_borsuk_6,d2_membered,d2_membered,d1_borsuk_6]), [file(borsuk_6,t18_borsuk_6),interesting(0.56)]). fof(t86_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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) => ( r4_borsuk_2(A,B,C,D,E) => r4_borsuk_2(A,C,B,k2_borsuk_2(A,B,C,D),k2_borsuk_2(A,B,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t85_borsuk_6]), [file(borsuk_6,t86_borsuk_6),interesting(0.56)]). fof(t6_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ( r1_xreal_0(A,k6_real_1(1,2)) => m1_subset_1(k3_xcmplx_0(2,A),u1_struct_0(k5_topmetr)) ) ) ), inference(mizar_proof,[status(thm)],[t66_xreal_1,t2_jordan5a,t66_xreal_1,t2_jordan5a]), [file(borsuk_6,t6_borsuk_6),interesting(0.55)]). fof(t67_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => ( r2_hidden(A,k6_borsuk_6) => r1_xreal_0(k1_mcart_1(A),k6_real_1(1,2)) ) ) ), inference(mizar_proof,[status(thm)],[d10_borsuk_6,t2_jordan5a,t21_xreal_1,t73_real_1,t8_mcart_1,t33_zfmisc_1]), [file(borsuk_6,t67_borsuk_6),interesting(0.55)]). fof(t68_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => ( r2_hidden(A,k8_borsuk_6) => r1_xreal_0(k6_real_1(1,2),k1_mcart_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d12_borsuk_6,t2_jordan5a,t21_xreal_1,t73_real_1,t8_mcart_1,t33_zfmisc_1]), [file(borsuk_6,t68_borsuk_6),interesting(0.55)]). fof(t9_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => m1_subset_1(k3_xcmplx_0(k6_real_1(1,2),A),u1_struct_0(k5_topmetr)) ) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t66_xreal_1,t2_jordan5a,t66_xreal_1,t2_xreal_1,t2_jordan5a]), [file(borsuk_6,t9_borsuk_6),interesting(0.54)]). fof(t5_borsuk_6,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,C) & r1_xreal_0(C,B) ) => r2_hidden(k7_xcmplx_0(k6_xcmplx_0(C,A),k6_xcmplx_0(B,A)),u1_struct_0(k4_topmetr(0,1))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_xreal_1,t2_xreal_1,t50_xreal_1,t49_xcmplx_1,t117_real_2,t50_xreal_1,t50_xreal_1,t125_real_2,t48_rcomp_1,t25_topmetr]), [file(borsuk_6,t5_borsuk_6),interesting(0.54)]). fof(t7_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ( r1_xreal_0(k6_real_1(1,2),A) => m1_subset_1(k6_xcmplx_0(k3_xcmplx_0(2,A),1),u1_struct_0(k5_topmetr)) ) ) ), inference(mizar_proof,[status(thm)],[t66_xreal_1,t11_xreal_1,t2_jordan5a,t66_xreal_1,t11_xreal_1,t2_jordan5a]), [file(borsuk_6,t7_borsuk_6),interesting(0.53)]). fof(t79_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ( ~ r1_xreal_0(k6_real_1(1,2),A) => ( ~ r2_hidden(k4_tarski(A,0),k7_borsuk_6) & ~ r2_hidden(k4_tarski(A,0),k8_borsuk_6) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_borsuk_6,t33_zfmisc_1,t22_xreal_1,t73_real_1,d12_borsuk_6,t33_zfmisc_1,t21_xreal_1,t73_real_1]), [file(borsuk_6,t79_borsuk_6),interesting(0.52)]). fof(t96_borsuk_6,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) ) => ! [D] : ( ( v5_seqm_3(D) & m1_borsuk_2(D,A,B,B) ) => r3_borsuk_2(A,B,B,C,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t6_borsuk_2,t15_borsuk_2]), [file(borsuk_6,t96_borsuk_6),interesting(0.49)]). fof(t10_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ( r1_xreal_0(k6_real_1(1,2),A) => m1_subset_1(k6_xcmplx_0(A,k6_real_1(1,4)),u1_struct_0(k5_topmetr)) ) ) ), inference(mizar_proof,[status(thm)],[t2_xreal_1,t21_xreal_1,t2_jordan5a,t2_xreal_1,t22_xreal_1,t2_jordan5a]), [file(borsuk_6,t10_borsuk_6),interesting(0.46)]). fof(t51_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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) => D = k2_borsuk_2(A,C,B,k2_borsuk_2(A,B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t50_borsuk_6]), [file(borsuk_6,t51_borsuk_6),interesting(0.46)]). fof(t64_borsuk_6,theorem,( k4_subset_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),k4_subset_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),k6_borsuk_6,k7_borsuk_6),k8_borsuk_6) = k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(0,1),k1_rcomp_1(0,1)) ), inference(mizar_proof,[status(thm)],[t1_borsuk_6,d10_xboole_0,d3_tarski,t83_borsuk_1,t10_mcart_1,t23_mcart_1,d11_borsuk_6,d12_borsuk_6,d10_borsuk_6,d2_xboole_0,d2_xboole_0]), [file(borsuk_6,t64_borsuk_6),interesting(0.44)]). fof(t35_borsuk_6,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(B,C) => ( v1_xboole_0(k1_rcomp_1(B,C)) & v6_compts_1(k1_rcomp_1(B,C),A) & m1_subset_1(k1_rcomp_1(B,C),k1_zfmisc_1(u1_struct_0(A))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_rcomp_1]), [file(borsuk_6,t35_borsuk_6),interesting(0.43)]). fof(t15_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ( ( A = a_0_2_borsuk_6 & B = a_0_3_borsuk_6 ) => k4_pre_topc(k15_euclid(2),k15_euclid(2),k2_jgraph_2(1,0,k6_real_1(1,2),k6_real_1(1,2)),A) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d12_funct_1,d2_jgraph_2,t56_euclid,t56_euclid,t66_xreal_1,t8_xreal_1,d10_xboole_0,d3_tarski,t36_jordan1k,d3_funct_2,d5_funct_1,d1_funct_2,d2_jgraph_2,t56_euclid,t56_euclid,t66_xreal_1,t11_xreal_1,d12_funct_1]), [file(borsuk_6,t15_borsuk_6),interesting(0.43)]). fof(t14_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ( ( A = a_0_0_borsuk_6 & B = a_0_1_borsuk_6 ) => k4_pre_topc(k15_euclid(2),k15_euclid(2),k2_jgraph_2(1,0,k6_real_1(1,2),k6_real_1(1,2)),A) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d12_funct_1,d2_jgraph_2,t56_euclid,t56_euclid,t66_xreal_1,t8_xreal_1,d10_xboole_0,d3_tarski,t36_jordan1k,d3_funct_2,d5_funct_1,d1_funct_2,d2_jgraph_2,t56_euclid,t56_euclid,t66_xreal_1,t11_xreal_1,d12_funct_1]), [file(borsuk_6,t14_borsuk_6),interesting(0.43)]). fof(t17_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ( ( A = a_0_6_borsuk_6 & B = a_0_7_borsuk_6 ) => k4_pre_topc(k15_euclid(2),k15_euclid(2),k2_jgraph_2(1,0,k6_real_1(1,2),k1_real_1(k6_real_1(1,2))),A) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d12_funct_1,d2_jgraph_2,t56_euclid,t66_xreal_1,t8_xreal_1,t56_euclid,d10_xboole_0,d3_tarski,t36_jordan1k,d3_funct_2,d5_funct_1,d1_funct_2,d2_jgraph_2,t56_euclid,t56_euclid,t66_xreal_1,t8_xreal_1,d12_funct_1]), [file(borsuk_6,t17_borsuk_6),interesting(0.40)]). fof(t16_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) => ( ( A = a_0_4_borsuk_6 & B = a_0_5_borsuk_6 ) => k4_pre_topc(k15_euclid(2),k15_euclid(2),k2_jgraph_2(1,0,k6_real_1(1,2),k1_real_1(k6_real_1(1,2))),A) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d12_funct_1,d2_jgraph_2,t56_euclid,t66_xreal_1,t8_xreal_1,t56_euclid,d10_xboole_0,d3_tarski,t36_jordan1k,d3_funct_2,d5_funct_1,d1_funct_2,d2_jgraph_2,t56_euclid,t56_euclid,t66_xreal_1,t8_xreal_1,d12_funct_1]), [file(borsuk_6,t16_borsuk_6),interesting(0.40)]). fof(t44_borsuk_6,theorem,( ! [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) => ( ( k1_funct_1(D,0) = B & k1_funct_1(D,1) = C ) => ( k1_funct_1(k5_relat_1(k3_treal_1(0,1,k2_treal_1(0,1),k1_treal_1(0,1)),D),0) = C & k1_funct_1(k5_relat_1(k3_treal_1(0,1,k2_treal_1(0,1),k1_treal_1(0,1)),D),1) = B ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_treal_1,t12_treal_1,d2_treal_1,d2_treal_1,t12_treal_1,d1_treal_1,t25_topmetr,t48_rcomp_1,t21_funct_2,t48_rcomp_1,t21_funct_2]), [file(borsuk_6,t44_borsuk_6),interesting(0.35)]). fof(t24_borsuk_6,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k6_borsuk_1(k3_topmetr,k3_topmetr)),u1_struct_0(k15_euclid(2))) & m2_relset_1(A,u1_struct_0(k6_borsuk_1(k3_topmetr,k3_topmetr)),u1_struct_0(k15_euclid(2))) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k1_funct_1(A,k4_tarski(B,C)) = k10_finseq_1(B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_catalg_1,d1_euclid,s7_funct_2,d5_borsuk_1,t25_euclid,t24_topmetr]), [file(borsuk_6,t24_borsuk_6),interesting(0.35)]). fof(t45_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( 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 ) => ( v5_pre_topc(k2_borsuk_2(A,B,C,D),k5_topmetr,A) & k1_funct_1(k2_borsuk_2(A,B,C,D),0) = C & k1_funct_1(k2_borsuk_2(A,B,C,D),1) = B ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_borsuk_6,t44_borsuk_6,d1_borsuk_2,d2_borsuk_2]), [file(borsuk_6,t45_borsuk_6),interesting(0.30)]). fof(t53_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) & v5_pre_topc(E,k5_topmetr,k5_topmetr) & m2_relset_1(E,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) ) => ( ( k1_funct_1(E,0) = 0 & k1_funct_1(E,1) = 1 & r1_borsuk_6(A,B,C) ) => r3_borsuk_2(A,B,C,k2_borsuk_6(A,B,C,D,E),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_jordan5a,t12_borsuk_6,t40_yellow12,t4_jordan5b,t106_zfmisc_1,d1_funct_2,t23_funct_1,d6_funct_3,d5_borsuk_6,t91_tmap_1,t39_yellow12,t106_zfmisc_1,d1_funct_2,t23_funct_1,d5_funct_3,t39_yellow12,t40_yellow12,t8_borsuk_6,t8_borsuk_6,t40_borsuk_6,t40_borsuk_6,d5_funct_3,d6_funct_3,d5_borsuk_1,d2_zfmisc_1,t83_borsuk_1,t48_rcomp_1,t2_jgraph_6,t83_borsuk_1,t48_rcomp_1,t83_borsuk_1,t48_rcomp_1,t2_xreal_1,t83_borsuk_1,t48_rcomp_1,t4_jordan5b,t2_jordan5a,t2_jgraph_6,t83_borsuk_1,t48_rcomp_1,t83_borsuk_1,t48_rcomp_1,t2_xreal_1,t83_borsuk_1,t48_rcomp_1,t41_borsuk_6,t2_jordan5a,t2_jordan5a,d1_funct_2,d5_borsuk_1,d2_borsuk_2,t58_tops_2,t2_jordan5a,t106_zfmisc_1,t2_jordan5a,t106_zfmisc_1,d1_funct_2,t23_funct_1,t23_funct_1,d6_borsuk_6,t23_funct_1,t2_jordan5a,t106_zfmisc_1,t2_jordan5a,t106_zfmisc_1,t23_funct_1,d2_borsuk_2,t23_funct_1,d2_borsuk_2,d7_borsuk_2]), [file(borsuk_6,t53_borsuk_6),interesting(0.30)]). fof(t40_borsuk_6,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(B,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ~ ( v5_pre_topc(A,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) & v5_pre_topc(B,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) & ! [C] : ( m1_subset_1(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => m1_subset_1(k3_xcmplx_0(k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),A,C),k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),B,C)),u1_struct_0(k5_topmetr)) ) & ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ~ ( ! [D] : ( m1_subset_1(D,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => ! [E] : ( v1_xreal_0(E) => ! [F] : ( v1_xreal_0(F) => ( ( k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),A,D) = E & k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),B,D) = F ) => k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),C,D) = k3_xcmplx_0(E,F) ) ) ) ) & v5_pre_topc(C,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t83_borsuk_1,t9_funct_2,t24_topmetr,t7_topmetr,t35_jgraph_2,t24_topmetr,t48_rcomp_1,t1_jordan1,d3_tarski,d5_funct_1,d1_funct_2,t83_borsuk_1,d1_funct_2,t4_funct_2,d16_borsuk_1,d7_topmetr,t63_jgraph_1]), [file(borsuk_6,t40_borsuk_6),interesting(0.21)]). fof(t41_borsuk_6,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(B,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ~ ( v5_pre_topc(A,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) & v5_pre_topc(B,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) & ! [C] : ( m1_subset_1(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => m1_subset_1(k2_xcmplx_0(k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),A,C),k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),B,C)),u1_struct_0(k5_topmetr)) ) & ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ~ ( ! [D] : ( m1_subset_1(D,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => ! [E] : ( v1_xreal_0(E) => ! [F] : ( v1_xreal_0(F) => ( ( k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),A,D) = E & k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),B,D) = F ) => k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),C,D) = k2_xcmplx_0(E,F) ) ) ) ) & v5_pre_topc(C,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t83_borsuk_1,t9_funct_2,t24_topmetr,t7_topmetr,t29_jgraph_2,t24_topmetr,t48_rcomp_1,t1_jordan1,d3_tarski,d5_funct_1,d1_funct_2,t83_borsuk_1,d1_funct_2,t4_funct_2,d16_borsuk_1,d7_topmetr,t63_jgraph_1]), [file(borsuk_6,t41_borsuk_6),interesting(0.21)]). fof(t54_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) & v5_pre_topc(E,k5_topmetr,k5_topmetr) & m2_relset_1(E,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) ) => ( ( k1_funct_1(E,0) = 0 & k1_funct_1(E,1) = 1 ) => r4_borsuk_2(A,B,C,k2_borsuk_6(A,B,C,D,E),D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t53_borsuk_6]), [file(borsuk_6,t54_borsuk_6),interesting(0.17)]). fof(t43_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ( v5_pre_topc(D,k5_topmetr,A) => ( v1_funct_1(k5_relat_1(k3_treal_1(0,1,k2_treal_1(0,1),k1_treal_1(0,1)),D)) & v1_funct_2(k5_relat_1(k3_treal_1(0,1,k2_treal_1(0,1),k1_treal_1(0,1)),D),u1_struct_0(k5_topmetr),u1_struct_0(A)) & v5_pre_topc(k5_relat_1(k3_treal_1(0,1,k2_treal_1(0,1),k1_treal_1(0,1)),D),k5_topmetr,A) & m2_relset_1(k5_relat_1(k3_treal_1(0,1,k2_treal_1(0,1),k1_treal_1(0,1)),D),u1_struct_0(k5_topmetr),u1_struct_0(A)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_treal_1,t27_topmetr,t58_tops_2]), [file(borsuk_6,t43_borsuk_6),interesting(0.13)]). fof(s1_recdef_2,theorem, ( ( ! [A] : ( r2_hidden(A,f1_s1_recdef_2) => ( ~ ( p1_s1_recdef_2(A) & p2_s1_recdef_2(A) ) & ~ ( p1_s1_recdef_2(A) & p3_s1_recdef_2(A) ) & ~ ( p2_s1_recdef_2(A) & p3_s1_recdef_2(A) ) ) ) & ! [A] : ~ ( r2_hidden(A,f1_s1_recdef_2) & ~ p1_s1_recdef_2(A) & ~ p2_s1_recdef_2(A) & ~ p3_s1_recdef_2(A) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s1_recdef_2 & ! [B] : ( r2_hidden(B,f1_s1_recdef_2) => ( ( p1_s1_recdef_2(B) => k1_funct_1(A,B) = f2_s1_recdef_2(B) ) & ( p2_s1_recdef_2(B) => k1_funct_1(A,B) = f3_s1_recdef_2(B) ) & ( p3_s1_recdef_2(B) => k1_funct_1(A,B) = f4_s1_recdef_2(B) ) ) ) ) ), file(recdef_2,s1_recdef_2), [interesting(0.00)]). fof(s1_borsuk_6,theorem, ( ( ! [A] : ( m1_subset_1(A,f1_s1_borsuk_6) => ( ~ ( p1_s1_borsuk_6(A) & p2_s1_borsuk_6(A) ) & ~ ( p1_s1_borsuk_6(A) & p3_s1_borsuk_6(A) ) & ~ ( p2_s1_borsuk_6(A) & p3_s1_borsuk_6(A) ) ) ) & ! [A] : ( m1_subset_1(A,f1_s1_borsuk_6) => ~ ( ~ p1_s1_borsuk_6(A) & ~ p2_s1_borsuk_6(A) & ~ p3_s1_borsuk_6(A) ) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s1_borsuk_6 & ! [B] : ( m1_subset_1(B,f1_s1_borsuk_6) => ( ( p1_s1_borsuk_6(B) => k1_funct_1(A,B) = f2_s1_borsuk_6(B) ) & ( p2_s1_borsuk_6(B) => k1_funct_1(A,B) = f3_s1_borsuk_6(B) ) & ( p3_s1_borsuk_6(B) => k1_funct_1(A,B) = f4_s1_borsuk_6(B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s1_recdef_2]), [file(borsuk_6,s1_borsuk_6),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(t21_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k2_xcmplx_0(A,B),C) <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ), file(xreal_1,t21_xreal_1), [interesting(0.00)]). fof(t2_jordan5a,theorem,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) ) <=> r2_hidden(A,u1_struct_0(k5_topmetr)) ) ) ), file(jordan5a,t2_jordan5a), [interesting(0.00)]). fof(t22_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,k2_xcmplx_0(B,C)) <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ), file(xreal_1,t22_xreal_1), [interesting(0.00)]). fof(t11_borsuk_6,theorem,( $true ), file(borsuk_6,t11_borsuk_6), [interesting(0.00)]). fof(d1_borsuk_6,definition,( ! [A] : ( l1_struct_0(A) => ( v1_borsuk_6(A) <=> v2_membered(u1_struct_0(A)) ) ) ), file(borsuk_6,d1_borsuk_6), [interesting(0.00)]). fof(d2_membered,definition,( ! [A] : ( v2_membered(A) <=> ! [B] : ( r2_hidden(B,A) => v1_xreal_0(B) ) ) ), file(membered,d2_membered), [interesting(0.00)]). fof(t2_borsuk_6,theorem,( $true ), file(borsuk_6,t2_borsuk_6), [interesting(0.00)]). fof(t43_borsuk_4,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => m1_subset_1(k1_rcomp_1(A,B),k1_zfmisc_1(u1_struct_0(k5_topmetr))) ) ) ), file(borsuk_4,t43_borsuk_4), [interesting(0.00)]). fof(t119_zfmisc_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ), file(zfmisc_1,t119_zfmisc_1), [interesting(0.00)]). fof(t48_rcomp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r2_hidden(C,k1_rcomp_1(A,B)) <=> ( r1_xreal_0(A,C) & r1_xreal_0(C,B) ) ) ) ) ) ), file(rcomp_1,t48_rcomp_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(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(t49_borsuk_4,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => ( r1_xreal_0(A,B) => ( ~ v1_xboole_0(k1_rcomp_1(A,B)) & v2_connsp_1(k1_rcomp_1(A,B),k5_topmetr) & v6_compts_1(k1_rcomp_1(A,B),k5_topmetr) & m1_subset_1(k1_rcomp_1(A,B),k1_zfmisc_1(u1_struct_0(k5_topmetr))) ) ) ) ) ), file(borsuk_4,t49_borsuk_4), [interesting(0.00)]). fof(t27_borsuk_3,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))) => ( ( v6_compts_1(C,A) & v6_compts_1(D,B) ) => ( v6_compts_1(k7_borsuk_1(A,B,C,D),k6_borsuk_1(A,B)) & m1_subset_1(k7_borsuk_1(A,B,C,D),k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) ) ) ) ) ) ) ), file(borsuk_3,t27_borsuk_3), [interesting(0.00)]). fof(t13_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => ! [C] : ( m1_subset_1(C,u1_struct_0(k5_topmetr)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k5_topmetr)) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => ( ~ v1_xboole_0(k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(A,B),k1_rcomp_1(C,D))) & v6_compts_1(k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(A,B),k1_rcomp_1(C,D)),k6_borsuk_1(k5_topmetr,k5_topmetr)) & m1_subset_1(k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(A,B),k1_rcomp_1(C,D)),k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_borsuk_4,t43_borsuk_4,t119_zfmisc_1,t48_rcomp_1,t48_rcomp_1,d5_borsuk_1,t106_zfmisc_1,t49_borsuk_4,t27_borsuk_3]), [file(borsuk_6,t13_borsuk_6),interesting(0.00)]). fof(t13_rcomp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(B,A) => k1_rcomp_1(B,A) = k1_xboole_0 ) ) ) ), file(rcomp_1,t13_rcomp_1), [interesting(0.00)]). fof(t34_borsuk_6,theorem,( ! [A] : ( l1_pre_topc(A) => ( v1_xboole_0(k1_xboole_0) & v6_compts_1(k1_xboole_0,A) & m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(A))) ) ) ), file(borsuk_6,t34_borsuk_6), [interesting(0.00)]). fof(t36_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => ! [C] : ( m1_subset_1(C,u1_struct_0(k5_topmetr)) => ! [D] : ( m1_subset_1(D,u1_struct_0(k5_topmetr)) => ( v6_compts_1(k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(A,B),k1_rcomp_1(C,D)),k6_borsuk_1(k5_topmetr,k5_topmetr)) & m1_subset_1(k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(A,B),k1_rcomp_1(C,D)),k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_borsuk_6,t35_borsuk_6,t34_borsuk_6,t35_borsuk_6,t34_borsuk_6,t35_borsuk_6,t34_borsuk_6]), [file(borsuk_6,t36_borsuk_6),interesting(0.00)]). fof(t3_borsuk_6,theorem,( $true ), file(borsuk_6,t3_borsuk_6), [interesting(0.00)]). fof(t83_borsuk_1,theorem,( u1_struct_0(k22_borsuk_1) = k1_rcomp_1(0,1) ), file(borsuk_1,t83_borsuk_1), [interesting(0.00)]). fof(t9_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( r1_tarski(B,C) => ( ( B = k1_xboole_0 & A != k1_xboole_0 ) | ( v1_funct_1(D) & v1_funct_2(D,A,C) & m2_relset_1(D,A,C) ) ) ) ) ), file(funct_2,t9_funct_2), [interesting(0.00)]). fof(t24_topmetr,theorem,( u1_struct_0(k3_topmetr) = k1_numbers ), file(topmetr,t24_topmetr), [interesting(0.00)]). fof(t7_topmetr,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [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(C)) & m2_relset_1(D,u1_struct_0(A),u1_struct_0(C)) ) => ( ( v5_pre_topc(D,A,C) & m1_pre_topc(C,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)) ) => ( E = D => v5_pre_topc(E,A,B) ) ) ) ) ) ) ) ), file(topmetr,t7_topmetr), [interesting(0.00)]). fof(t31_jgraph_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(A),u1_struct_0(k3_topmetr)) & m2_relset_1(B,u1_struct_0(A),u1_struct_0(k3_topmetr)) ) => ! [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)) ) => ~ ( v5_pre_topc(B,A,k3_topmetr) & v5_pre_topc(C,A,k3_topmetr) & ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),u1_struct_0(k3_topmetr)) & m2_relset_1(D,u1_struct_0(A),u1_struct_0(k3_topmetr)) ) => ~ ( ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( v1_xreal_0(F) => ! [G] : ( v1_xreal_0(G) => ( ( k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),B,E) = F & k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),C,E) = G ) => k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),D,E) = k6_xcmplx_0(F,G) ) ) ) ) & v5_pre_topc(D,A,k3_topmetr) ) ) ) ) ) ) ), file(jgraph_2,t31_jgraph_2), [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(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(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(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(t4_funct_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(k2_relat_1(B),A) => ( v1_funct_1(B) & v1_funct_2(B,k1_relat_1(B),A) & m2_relset_1(B,k1_relat_1(B),A) ) ) ) ), file(funct_2,t4_funct_2), [interesting(0.00)]). fof(d16_borsuk_1,definition,( ! [A] : ( l1_pre_topc(A) => ( A = k22_borsuk_1 <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k5_pcomps_1(k8_metric_1)))) => ( B = k1_rcomp_1(0,1) => A = k3_pre_topc(k5_pcomps_1(k8_metric_1),B) ) ) ) ) ), file(borsuk_1,d16_borsuk_1), [interesting(0.00)]). fof(d7_topmetr,definition,( k3_topmetr = k5_pcomps_1(k8_metric_1) ), file(topmetr,d7_topmetr), [interesting(0.00)]). fof(t63_jgraph_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] : ( ( 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)) ) => ! [D] : ( ( ~ v1_xboole_0(D) & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(A),u1_struct_0(k3_pre_topc(B,D))) & m2_relset_1(E,u1_struct_0(A),u1_struct_0(k3_pre_topc(B,D))) ) => ( ( C = E & v5_pre_topc(C,A,B) ) => v5_pre_topc(E,A,k3_pre_topc(B,D)) ) ) ) ) ) ) ), file(jgraph_1,t63_jgraph_1), [interesting(0.00)]). fof(t42_borsuk_6,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(A,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(B,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ~ ( v5_pre_topc(A,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) & v5_pre_topc(B,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) & ! [C] : ( m1_subset_1(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => m1_subset_1(k6_xcmplx_0(k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),A,C),k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),B,C)),u1_struct_0(k5_topmetr)) ) & ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) & m2_relset_1(C,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr)) ) => ~ ( ! [D] : ( m1_subset_1(D,u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) => ! [E] : ( v1_xreal_0(E) => ! [F] : ( v1_xreal_0(F) => ( ( k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),A,D) = E & k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),B,D) = F ) => k8_funct_2(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)),u1_struct_0(k5_topmetr),C,D) = k6_xcmplx_0(E,F) ) ) ) ) & v5_pre_topc(C,k6_borsuk_1(k5_topmetr,k5_topmetr),k5_topmetr) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t83_borsuk_1,t9_funct_2,t24_topmetr,t7_topmetr,t31_jgraph_2,t24_topmetr,t48_rcomp_1,t1_jordan1,d3_tarski,d5_funct_1,d1_funct_2,t83_borsuk_1,d1_funct_2,t4_funct_2,d16_borsuk_1,d7_topmetr,t63_jgraph_1]), [file(borsuk_6,t42_borsuk_6),interesting(0.00)]). fof(t11_treal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(A,B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(A,B))) => ( v1_funct_1(k3_treal_1(A,B,C,D)) & v1_funct_2(k3_treal_1(A,B,C,D),u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B))) & v5_pre_topc(k3_treal_1(A,B,C,D),k4_topmetr(0,1),k4_topmetr(A,B)) & m2_relset_1(k3_treal_1(A,B,C,D),u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B))) ) ) ) ) ) ) ), file(treal_1,t11_treal_1), [interesting(0.00)]). fof(t27_topmetr,theorem,( k4_topmetr(0,1) = k22_borsuk_1 ), file(topmetr,t27_topmetr), [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(d1_treal_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => k1_treal_1(A,B) = A ) ) ) ), file(treal_1,d1_treal_1), [interesting(0.00)]). fof(t12_treal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(A,B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(A,B))) => ( k8_funct_2(u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B)),k3_treal_1(A,B,C,D),k1_treal_1(0,1)) = C & k8_funct_2(u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B)),k3_treal_1(A,B,C,D),k2_treal_1(0,1)) = D ) ) ) ) ) ) ), file(treal_1,t12_treal_1), [interesting(0.00)]). fof(d2_treal_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => k2_treal_1(A,B) = B ) ) ) ), file(treal_1,d2_treal_1), [interesting(0.00)]). fof(t25_topmetr,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => u1_struct_0(k4_topmetr(A,B)) = k1_rcomp_1(A,B) ) ) ) ), file(topmetr,t25_topmetr), [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(d1_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)) & v5_pre_topc(D,k5_topmetr,A) & k1_funct_1(D,0) = B & k1_funct_1(D,1) = C ) ) ) ) ) ), file(borsuk_2,d1_borsuk_2), [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(t47_borsuk_6,theorem,( $true ), file(borsuk_6,t47_borsuk_6), [interesting(0.00)]). fof(t48_borsuk_6,theorem,( $true ), file(borsuk_6,t48_borsuk_6), [interesting(0.00)]). fof(t49_borsuk_6,theorem,( $true ), file(borsuk_6,t49_borsuk_6), [interesting(0.00)]). fof(t4_borsuk_6,theorem,( $true ), file(borsuk_6,t4_borsuk_6), [interesting(0.00)]). fof(d3_borsuk_2,definition,( ! [A] : ( l1_pre_topc(A) => ( v1_borsuk_2(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) ) ) ) ) ), file(borsuk_2,d3_borsuk_2), [interesting(0.00)]). fof(t4_jordan5b,theorem,( ! [A] : ( v1_xreal_0(A) => ( r2_hidden(A,u1_struct_0(k22_borsuk_1)) => r2_hidden(k6_xcmplx_0(1,A),u1_struct_0(k22_borsuk_1)) ) ) ), file(jordan5b,t4_jordan5b), [interesting(0.00)]). fof(d6_borsuk_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(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) => ( r2_borsuk_2(A,B,C) => ! [E] : ( m1_borsuk_2(E,A,C,B) => ( E = k2_borsuk_2(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k5_topmetr)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(A),E,F) = k1_funct_1(D,k6_xcmplx_0(1,F)) ) ) ) ) ) ) ) ) ), file(borsuk_2,d6_borsuk_2), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(t52_borsuk_6,theorem,( $true ), file(borsuk_6,t52_borsuk_6), [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(t91_tmap_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(tmap_1,t91_tmap_1), [interesting(0.00)]). fof(d4_borsuk_2,definition,( ! [A] : ( ( v1_borsuk_2(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [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,d4_borsuk_2), [interesting(0.00)]). fof(t40_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) ) => ( v1_funct_1(k10_funct_3(u1_struct_0(A),u1_struct_0(B))) & v1_funct_2(k10_funct_3(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(B)) & v5_pre_topc(k10_funct_3(u1_struct_0(A),u1_struct_0(B)),k6_borsuk_1(A,B),B) & m2_relset_1(k10_funct_3(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(B)) ) ) ) ), file(yellow12,t40_yellow12), [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(d6_funct_3,definition,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k8_funct_3(A,B) <=> ( k1_relat_1(C) = k2_zfmisc_1(A,B) & ! [D,E] : ( ( r2_hidden(D,A) & r2_hidden(E,B) ) => k1_funct_1(C,k4_tarski(D,E)) = E ) ) ) ) ), file(funct_3,d6_funct_3), [interesting(0.00)]). fof(d5_borsuk_6,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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,C,B) => ( E = k2_borsuk_2(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k5_topmetr)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(A),E,F) = k1_funct_1(D,k6_xcmplx_0(1,F)) ) ) ) ) ) ) ) ), file(borsuk_6,d5_borsuk_6), [interesting(0.00)]). fof(t39_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) ) => ( v1_funct_1(k9_funct_3(u1_struct_0(A),u1_struct_0(B))) & v1_funct_2(k9_funct_3(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(A)) & v5_pre_topc(k9_funct_3(u1_struct_0(A),u1_struct_0(B)),k6_borsuk_1(A,B),A) & m2_relset_1(k9_funct_3(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(A)) ) ) ) ), file(yellow12,t39_yellow12), [interesting(0.00)]). fof(d5_funct_3,definition,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k7_funct_3(A,B) <=> ( k1_relat_1(C) = k2_zfmisc_1(A,B) & ! [D,E] : ( ( r2_hidden(D,A) & r2_hidden(E,B) ) => k1_funct_1(C,k4_tarski(D,E)) = D ) ) ) ) ), file(funct_3,d5_funct_3), [interesting(0.00)]). fof(t121_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) | ( r1_xreal_0(A,0) & r1_xreal_0(B,0) ) ) => r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ) ), file(real_2,t121_real_2), [interesting(0.00)]). fof(t140_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(0,A) & r1_xreal_0(A,1) & r1_xreal_0(0,B) & r1_xreal_0(B,1) ) | ( r1_xreal_0(A,0) & r1_xreal_0(k4_xcmplx_0(1),A) & r1_xreal_0(B,0) & r1_xreal_0(k4_xcmplx_0(1),B) ) ) => r1_xreal_0(k3_xcmplx_0(A,B),1) ) ) ) ), file(real_2,t140_real_2), [interesting(0.00)]). fof(t35_jgraph_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(A),u1_struct_0(k3_topmetr)) & m2_relset_1(B,u1_struct_0(A),u1_struct_0(k3_topmetr)) ) => ! [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)) ) => ~ ( v5_pre_topc(B,A,k3_topmetr) & v5_pre_topc(C,A,k3_topmetr) & ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),u1_struct_0(k3_topmetr)) & m2_relset_1(D,u1_struct_0(A),u1_struct_0(k3_topmetr)) ) => ~ ( ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( v1_xreal_0(F) => ! [G] : ( v1_xreal_0(G) => ( ( k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),B,E) = F & k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),C,E) = G ) => k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),D,E) = k3_xcmplx_0(F,G) ) ) ) ) & v5_pre_topc(D,A,k3_topmetr) ) ) ) ) ) ) ), file(jgraph_2,t35_jgraph_2), [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(t2_jgraph_6,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(0,C) & r1_xreal_0(C,1) & r1_xreal_0(A,B) ) => ( r1_xreal_0(A,k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,C),A),k3_xcmplx_0(C,B))) & r1_xreal_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,C),A),k3_xcmplx_0(C,B)),B) ) ) ) ) ) ), file(jgraph_6,t2_jgraph_6), [interesting(0.00)]). fof(t29_jgraph_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(A),u1_struct_0(k3_topmetr)) & m2_relset_1(B,u1_struct_0(A),u1_struct_0(k3_topmetr)) ) => ! [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)) ) => ~ ( v5_pre_topc(B,A,k3_topmetr) & v5_pre_topc(C,A,k3_topmetr) & ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),u1_struct_0(k3_topmetr)) & m2_relset_1(D,u1_struct_0(A),u1_struct_0(k3_topmetr)) ) => ~ ( ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( v1_xreal_0(F) => ! [G] : ( v1_xreal_0(G) => ( ( k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),B,E) = F & k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),C,E) = G ) => k8_funct_2(u1_struct_0(A),u1_struct_0(k3_topmetr),D,E) = k2_xcmplx_0(F,G) ) ) ) ) & v5_pre_topc(D,A,k3_topmetr) ) ) ) ) ) ) ), file(jgraph_2,t29_jgraph_2), [interesting(0.00)]). fof(d6_borsuk_6,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(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] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) & v5_pre_topc(E,k5_topmetr,k5_topmetr) & m2_relset_1(E,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) ) => ( ( k1_funct_1(E,0) = 0 & k1_funct_1(E,1) = 1 & r1_borsuk_6(A,B,C) ) => k2_borsuk_6(A,B,C,D,E) = k7_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),u1_struct_0(A),E,D) ) ) ) ) ) ) ), file(borsuk_6,d6_borsuk_6), [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(t27_jordan20,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_borsuk_2(E,A,B,C) => ! [F] : ( m1_borsuk_2(F,A,C,D) => ( ( v5_pre_topc(E,k5_topmetr,A) & v5_pre_topc(F,k5_topmetr,A) & k1_funct_1(E,0) = B & k1_funct_1(E,1) = C & k1_funct_1(F,0) = C & k1_funct_1(F,1) = D ) => ( v5_pre_topc(k1_borsuk_2(A,B,C,D,E,F),k5_topmetr,A) & k1_funct_1(k1_borsuk_2(A,B,C,D,E,F),0) = B & k1_funct_1(k1_borsuk_2(A,B,C,D,E,F),1) = D ) ) ) ) ) ) ) ) ), file(jordan20,t27_jordan20), [interesting(0.00)]). fof(d9_borsuk_6,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) & m2_relset_1(A,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) ) => ( A = k5_borsuk_6 <=> ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => ( ( r1_xreal_0(B,k6_real_1(1,2)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),A,B) = k3_xcmplx_0(k6_real_1(1,2),B) ) & ( r1_xreal_0(B,k6_real_1(3,4)) => ( r1_xreal_0(B,k6_real_1(1,2)) | k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),A,B) = k6_xcmplx_0(B,k6_real_1(1,4)) ) ) & ( ~ r1_xreal_0(B,k6_real_1(3,4)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),A,B) = k6_xcmplx_0(k3_xcmplx_0(2,B),1) ) ) ) ) ) ), file(borsuk_6,d9_borsuk_6), [interesting(0.00)]). fof(t66_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(0,C) ) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t66_xreal_1), [interesting(0.00)]). fof(d5_borsuk_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(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_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_borsuk_2(E,A,B,C) => ! [F] : ( m1_borsuk_2(F,A,C,D) => ( ( r2_borsuk_2(A,B,C) & r2_borsuk_2(A,C,D) ) => ! [G] : ( m1_borsuk_2(G,A,B,D) => ( G = k1_borsuk_2(A,B,C,D,E,F) <=> ! [H] : ( m1_subset_1(H,u1_struct_0(k5_topmetr)) => ( ( r1_xreal_0(H,k6_real_1(1,2)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(A),G,H) = k1_funct_1(E,k3_xcmplx_0(2,H)) ) & ( r1_xreal_0(k6_real_1(1,2),H) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(A),G,H) = k1_funct_1(F,k6_xcmplx_0(k3_xcmplx_0(2,H),1)) ) ) ) ) ) ) ) ) ) ) ) ) ), file(borsuk_2,d5_borsuk_2), [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(t70_xreal_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(k3_xcmplx_0(C,A),k3_xcmplx_0(B,A)) ) ) ) ) ), file(xreal_1,t70_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(t60_borsuk_6,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_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_borsuk_2(F,A,B,C) => ! [G] : ( m1_borsuk_2(G,A,C,D) => ! [H] : ( m1_borsuk_2(H,A,D,E) => ( ( r1_borsuk_6(A,B,C) & r1_borsuk_6(A,C,D) & r1_borsuk_6(A,D,E) ) => k2_borsuk_6(A,B,E,k1_borsuk_2(A,B,D,E,k1_borsuk_2(A,B,C,D,F,G),H),k5_borsuk_6) = k1_borsuk_2(A,B,C,E,F,k1_borsuk_2(A,C,D,E,G,H)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_borsuk_6,t46_borsuk_6,d1_funct_2,t46_borsuk_6,d6_borsuk_6,t57_borsuk_6,t23_funct_1,t9_borsuk_6,t66_xreal_1,t2_xreal_1,d9_borsuk_6,d5_borsuk_2,d5_borsuk_2,d5_borsuk_2,t11_xreal_1,t2_xreal_1,t11_xreal_1,t2_jordan5a,t6_borsuk_6,t66_xreal_1,t7_borsuk_6,t66_xreal_1,t11_xreal_1,d9_borsuk_6,d5_borsuk_2,d5_borsuk_2,d5_borsuk_2,d5_borsuk_2,t2_xreal_1,t7_borsuk_6,t70_xreal_1,t92_real_1,t7_borsuk_6,d9_borsuk_6,d5_borsuk_2,d5_borsuk_2,d5_borsuk_2,t113_funct_2]), [file(borsuk_6,t60_borsuk_6),interesting(0.00)]). fof(t81_borsuk_6,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_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_borsuk_2(F,A,B,C) => ! [G] : ( m1_borsuk_2(G,A,C,D) => ! [H] : ( m1_borsuk_2(H,A,D,E) => ( ( r1_borsuk_6(A,B,C) & r1_borsuk_6(A,C,D) & r1_borsuk_6(A,D,E) ) => r3_borsuk_2(A,B,E,k1_borsuk_2(A,B,D,E,k1_borsuk_2(A,B,C,D,F,G),H),k1_borsuk_2(A,B,C,E,F,k1_borsuk_2(A,C,D,E,G,H))) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_borsuk_6,t46_borsuk_6,t60_borsuk_6,t53_borsuk_6,t57_borsuk_6]), [file(borsuk_6,t81_borsuk_6),interesting(0.00)]). fof(t82_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_borsuk_2(F,A,B,C) => ! [G] : ( m1_borsuk_2(G,A,C,D) => ! [H] : ( m1_borsuk_2(H,A,D,E) => r4_borsuk_2(A,B,E,k1_borsuk_2(A,B,D,E,k1_borsuk_2(A,B,C,D,F,G),H),k1_borsuk_2(A,B,C,E,F,k1_borsuk_2(A,C,D,E,G,H))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t81_borsuk_6]), [file(borsuk_6,t82_borsuk_6),interesting(0.00)]). fof(t15_treal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(0,1))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(0,1))) => ( v1_funct_1(k4_treal_1(A,B,C,D)) & v1_funct_2(k4_treal_1(A,B,C,D),u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1))) & v5_pre_topc(k4_treal_1(A,B,C,D),k4_topmetr(A,B),k4_topmetr(0,1)) & m2_relset_1(k4_treal_1(A,B,C,D),u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1))) ) ) ) ) ) ) ), file(treal_1,t15_treal_1), [interesting(0.00)]). fof(t38_borsuk_6,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( r1_xreal_0(C,D) => ( r1_xreal_0(B,A) | ( v1_funct_1(k1_borsuk_6(A,B,C,D)) & v1_funct_2(k1_borsuk_6(A,B,C,D),u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(C,D))) & v5_pre_topc(k1_borsuk_6(A,B,C,D),k4_topmetr(A,B),k4_topmetr(C,D)) & m2_relset_1(k1_borsuk_6(A,B,C,D),u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(C,D))) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_treal_1,t15_treal_1,t58_tops_2]), [file(borsuk_6,t38_borsuk_6),interesting(0.00)]). fof(t12_borsuk_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] : ( ( ~ v3_struct_0(C) & v2_pre_topc(C) & l1_pre_topc(C) ) => ! [D] : ( ( ~ v3_struct_0(D) & v2_pre_topc(D) & l1_pre_topc(D) ) => ! [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)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,u1_struct_0(B),u1_struct_0(D)) & v5_pre_topc(F,B,D) & m2_relset_1(F,u1_struct_0(B),u1_struct_0(D)) ) => v5_pre_topc(k3_borsuk_2(A,C,B,D,E,F),k6_borsuk_1(A,B),k6_borsuk_1(C,D)) ) ) ) ) ) ) ), file(borsuk_2,t12_borsuk_2), [interesting(0.00)]). fof(d3_pre_topc,definition,( ! [A] : ( l1_struct_0(A) => k2_pre_topc(A) = u1_struct_0(A) ) ), file(pre_topc,d3_pre_topc), [interesting(0.00)]). fof(t31_waybel34,theorem,( ! [A] : ( l1_pre_topc(A) => k3_pre_topc(A,k2_pre_topc(A)) = g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) ) ), file(waybel34,t31_waybel34), [interesting(0.00)]). fof(t7_jgraph_5,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k5_topmetr))) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,B) & r1_xreal_0(B,1) & C = k1_rcomp_1(A,B) ) => k4_topmetr(A,B) = k3_pre_topc(k5_topmetr,C) ) ) ) ) ), file(jgraph_5,t7_jgraph_5), [interesting(0.00)]). fof(t26_borsuk_3,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(B,A)))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(B))) => ( C = k7_borsuk_1(B,A,E,D) => g1_pre_topc(u1_struct_0(k6_borsuk_1(k3_pre_topc(B,E),k3_pre_topc(A,D))),u1_pre_topc(k6_borsuk_1(k3_pre_topc(B,E),k3_pre_topc(A,D)))) = g1_pre_topc(u1_struct_0(k3_pre_topc(k6_borsuk_1(B,A),C)),u1_pre_topc(k3_pre_topc(k6_borsuk_1(B,A),C))) ) ) ) ) ) ) ), file(borsuk_3,t26_borsuk_3), [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(t120_zfmisc_1,theorem,( ! [A,B,C] : ( k2_zfmisc_1(k2_xboole_0(A,B),C) = k2_xboole_0(k2_zfmisc_1(A,C),k2_zfmisc_1(B,C)) & k2_zfmisc_1(C,k2_xboole_0(A,B)) = k2_xboole_0(k2_zfmisc_1(C,A),k2_zfmisc_1(C,B)) ) ), file(zfmisc_1,t120_zfmisc_1), [interesting(0.00)]). fof(t2_treal_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(B,C) ) => k4_subset_1(k1_numbers,k1_rcomp_1(A,C),k1_rcomp_1(B,D)) = k1_rcomp_1(A,D) ) ) ) ) ) ), file(treal_1,t2_treal_1), [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(t32_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) => ( ( A = k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(0,k6_real_1(1,2)),k1_rcomp_1(0,1)) & B = k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(k6_real_1(1,2),1),k1_rcomp_1(0,1)) ) => k2_xboole_0(k2_pre_topc(k3_pre_topc(k6_borsuk_1(k5_topmetr,k5_topmetr),A)),k2_pre_topc(k3_pre_topc(k6_borsuk_1(k5_topmetr,k5_topmetr),B))) = k2_pre_topc(k6_borsuk_1(k5_topmetr,k5_topmetr)) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_pre_topc,d10_pre_topc,t120_zfmisc_1,t2_treal_1,t83_borsuk_1,d5_borsuk_1,t12_pre_topc]), [file(borsuk_6,t32_borsuk_6),interesting(0.00)]). fof(t122_zfmisc_1,theorem,( ! [A,B,C] : ( k2_zfmisc_1(k3_xboole_0(A,B),C) = k3_xboole_0(k2_zfmisc_1(A,C),k2_zfmisc_1(B,C)) & k2_zfmisc_1(C,k3_xboole_0(A,B)) = k3_xboole_0(k2_zfmisc_1(C,A),k2_zfmisc_1(C,B)) ) ), file(zfmisc_1,t122_zfmisc_1), [interesting(0.00)]). fof(t1_topmetr2,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) ) => k5_subset_1(k1_numbers,k1_rcomp_1(A,B),k1_rcomp_1(B,C)) = k1_tarski(B) ) ) ) ) ), file(topmetr2,t1_topmetr2), [interesting(0.00)]). fof(t33_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) => ( ( A = k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(0,k6_real_1(1,2)),k1_rcomp_1(0,1)) & B = k12_mcart_1(k1_numbers,k1_numbers,k1_rcomp_1(k6_real_1(1,2),1),k1_rcomp_1(0,1)) ) => k3_xboole_0(k2_pre_topc(k3_pre_topc(k6_borsuk_1(k5_topmetr,k5_topmetr),A)),k2_pre_topc(k3_pre_topc(k6_borsuk_1(k5_topmetr,k5_topmetr),B))) = k2_zfmisc_1(k1_tarski(k6_real_1(1,2)),k1_rcomp_1(0,1)) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_pre_topc,d10_pre_topc,t122_zfmisc_1,t1_topmetr2]), [file(borsuk_6,t33_borsuk_6),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(t16_treal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(0,1))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(0,1))) => ( k8_funct_2(u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1)),k4_treal_1(A,B,C,D),k1_treal_1(A,B)) = C & k8_funct_2(u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1)),k4_treal_1(A,B,C,D),k2_treal_1(A,B)) = D ) ) ) ) ) ) ), file(treal_1,t16_treal_1), [interesting(0.00)]). fof(t86_funct_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C,D] : ( r2_hidden(k4_tarski(C,D),k2_zfmisc_1(k1_relat_1(A),k1_relat_1(B))) => k1_funct_1(k15_funct_3(A,B),k4_tarski(C,D)) = k4_tarski(k1_funct_1(A,C),k1_funct_1(B,D)) ) ) ) ), file(funct_3,t86_funct_3), [interesting(0.00)]). fof(t1_borsuk_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] : ( ( ~ v3_struct_0(C) & v2_pre_topc(C) & l1_pre_topc(C) ) => ! [D] : ( ( ~ v3_struct_0(D) & v2_pre_topc(D) & l1_pre_topc(D) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,u1_struct_0(C),u1_struct_0(B)) & m2_relset_1(F,u1_struct_0(C),u1_struct_0(B)) ) => ~ ( m1_pre_topc(A,D) & m1_pre_topc(C,D) & k2_xboole_0(k2_pre_topc(A),k2_pre_topc(C)) = k2_pre_topc(D) & v2_compts_1(A) & v2_compts_1(C) & v3_compts_1(D) & v5_pre_topc(E,A,B) & v5_pre_topc(F,C,B) & ! [G] : ( r2_hidden(G,k3_xboole_0(k2_pre_topc(A),k2_pre_topc(C))) => k1_funct_1(E,G) = k1_funct_1(F,G) ) & ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,u1_struct_0(D),u1_struct_0(B)) & m2_relset_1(G,u1_struct_0(D),u1_struct_0(B)) ) => ~ ( G = k1_funct_4(E,F) & v5_pre_topc(G,D,B) ) ) ) ) ) ) ) ) ) ), file(borsuk_2,t1_borsuk_2), [interesting(0.00)]). fof(t50_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ), file(xreal_1,t50_xreal_1), [interesting(0.00)]). fof(t49_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k7_xcmplx_0(A,0) = 0 ) ), file(xcmplx_1,t49_xcmplx_1), [interesting(0.00)]). fof(t117_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(A,0) => ( ~ ( ~ r1_xreal_0(k7_xcmplx_0(B,A),1) & r1_xreal_0(B,A) ) & ~ ( ~ r1_xreal_0(1,k7_xcmplx_0(B,A)) & r1_xreal_0(A,B) ) & ( ~ r1_xreal_0(k7_xcmplx_0(B,A),k4_xcmplx_0(1)) => ( ~ r1_xreal_0(B,k4_xcmplx_0(A)) & ~ r1_xreal_0(A,k4_xcmplx_0(B)) ) ) & ( ~ r1_xreal_0(k4_xcmplx_0(1),k7_xcmplx_0(B,A)) => ( ~ r1_xreal_0(k4_xcmplx_0(A),B) & ~ r1_xreal_0(k4_xcmplx_0(B),A) ) ) ) ) ) ) ), file(real_2,t117_real_2), [interesting(0.00)]). fof(t125_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(A,0) & r1_xreal_0(B,0) ) | ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) ) => r1_xreal_0(0,k7_xcmplx_0(A,B)) ) ) ) ), file(real_2,t125_real_2), [interesting(0.00)]). fof(d4_treal_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(0,1))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(0,1))) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1))) & m2_relset_1(E,u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1))) ) => ( E = k4_treal_1(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k4_topmetr(A,B))) => ! [G] : ( v1_xreal_0(G) => ! [H] : ( v1_xreal_0(H) => ! [I] : ( v1_xreal_0(I) => ( ( F = G & H = C & I = D ) => k8_funct_2(u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1)),E,F) = k7_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(B,G),H),k3_xcmplx_0(k6_xcmplx_0(G,A),I)),k6_xcmplx_0(B,A)) ) ) ) ) ) ) ) ) ) ) ) ) ), file(treal_1,d4_treal_1), [interesting(0.00)]). fof(d3_treal_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(A,B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(A,B))) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B))) & m2_relset_1(E,u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B))) ) => ( E = k3_treal_1(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k4_topmetr(0,1))) => ! [G] : ( v1_xreal_0(G) => ! [H] : ( v1_xreal_0(H) => ! [I] : ( v1_xreal_0(I) => ( ( F = G & H = C & I = D ) => k8_funct_2(u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B)),E,F) = k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,G),H),k3_xcmplx_0(G,I)) ) ) ) ) ) ) ) ) ) ) ) ) ), file(treal_1,d3_treal_1), [interesting(0.00)]). fof(t236_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => k2_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(k6_xcmplx_0(A,B),C),D),B) = k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,k7_xcmplx_0(D,C)),B),k3_xcmplx_0(k7_xcmplx_0(D,C),A)) ) ) ) ) ), file(xcmplx_1,t236_xcmplx_1), [interesting(0.00)]). fof(l2_borsuk_6,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ! [D] : ( v1_xcmplx_0(D) => k2_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(k6_xcmplx_0(D,C),B),A),C) = k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(1,k7_xcmplx_0(A,B)),C),k3_xcmplx_0(k7_xcmplx_0(A,B),D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t236_xcmplx_1]), [file(borsuk_6,l2_borsuk_6),interesting(0.00)]). fof(t39_borsuk_6,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( r1_xreal_0(C,D) => ( r1_xreal_0(B,A) | ! [E] : ( v1_xreal_0(E) => ( ( r1_xreal_0(A,E) & r1_xreal_0(E,B) ) => k1_funct_1(k1_borsuk_6(A,B,C,D),E) = k2_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(k6_xcmplx_0(D,C),k6_xcmplx_0(B,A)),k6_xcmplx_0(E,A)),C) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_treal_1,d2_treal_1,t48_rcomp_1,t25_topmetr,d1_funct_2,d1_treal_1,d2_treal_1,t5_borsuk_6,t23_funct_1,d4_treal_1,d3_treal_1,l2_borsuk_6]), [file(borsuk_6,t39_borsuk_6),interesting(0.00)]). fof(t12_funct_4,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(k1_funct_4(C,B),A) = k1_funct_1(C,A) ) ) ) ), file(funct_4,t12_funct_4), [interesting(0.00)]). fof(t14_funct_4,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(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ), file(funct_4,t14_funct_4), [interesting(0.00)]). fof(t83_borsuk_6,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_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_borsuk_2(E,A,B,C) => ! [F] : ( m1_borsuk_2(F,A,B,C) => ! [G] : ( m1_borsuk_2(G,A,C,D) => ! [H] : ( m1_borsuk_2(H,A,C,D) => ( ( r1_borsuk_6(A,B,C) & r1_borsuk_6(A,C,D) & r3_borsuk_2(A,B,C,E,F) & r3_borsuk_2(A,C,D,G,H) ) => r3_borsuk_2(A,B,D,k1_borsuk_2(A,B,C,D,E,G),k1_borsuk_2(A,B,C,D,F,H)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_borsuk_2,d7_borsuk_2,t38_borsuk_6,t27_topmetr,t38_borsuk_6,t27_topmetr,t2_jordan5a,t13_borsuk_6,t13_borsuk_6,t12_borsuk_2,t49_borsuk_4,t49_borsuk_4,t49_borsuk_4,t83_borsuk_1,d3_pre_topc,t31_waybel34,t7_jgraph_5,t26_borsuk_3,t58_tops_2,t12_borsuk_2,t7_jgraph_5,t26_borsuk_3,t58_tops_2,t32_borsuk_6,d1_funct_2,d5_borsuk_1,d1_funct_2,d5_borsuk_1,d1_funct_2,d5_borsuk_1,t33_borsuk_6,d2_zfmisc_1,t25_topmetr,t27_topmetr,t25_topmetr,t27_topmetr,d1_tarski,t48_rcomp_1,t25_topmetr,t106_zfmisc_1,d5_borsuk_1,d1_funct_2,t48_rcomp_1,t25_topmetr,t106_zfmisc_1,d5_borsuk_1,d1_funct_2,d1_funct_2,d1_funct_2,t106_zfmisc_1,d1_funct_2,t106_zfmisc_1,t37_borsuk_6,t37_borsuk_6,t23_funct_1,t86_funct_3,t91_tmap_1,t91_tmap_1,t86_funct_3,t23_funct_1,t1_borsuk_2,d7_borsuk_2,t2_jordan5a,t48_rcomp_1,t25_topmetr,t106_zfmisc_1,t48_rcomp_1,t2_jordan5a,t25_topmetr,t106_zfmisc_1,d1_funct_2,d1_funct_2,t106_zfmisc_1,t39_borsuk_6,t6_borsuk_6,t12_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,d5_borsuk_2,t2_jordan5a,t48_rcomp_1,t2_jordan5a,t25_topmetr,t106_zfmisc_1,t106_zfmisc_1,d1_funct_2,d1_funct_2,t106_zfmisc_1,t39_borsuk_6,t7_borsuk_6,t14_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,d5_borsuk_2,t2_jordan5a,t48_rcomp_1,t25_topmetr,t106_zfmisc_1,t48_rcomp_1,t2_jordan5a,t25_topmetr,t106_zfmisc_1,d1_funct_2,d1_funct_2,t106_zfmisc_1,t39_borsuk_6,t6_borsuk_6,t12_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,d5_borsuk_2,t2_jordan5a,t48_rcomp_1,t2_jordan5a,t25_topmetr,t106_zfmisc_1,t106_zfmisc_1,d1_funct_2,d1_funct_2,t106_zfmisc_1,t39_borsuk_6,t7_borsuk_6,t14_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,d5_borsuk_2,d1_funct_2,d5_borsuk_1,t48_rcomp_1,t25_topmetr,t106_zfmisc_1,t48_rcomp_1,t25_topmetr,t106_zfmisc_1,t48_rcomp_1,t25_topmetr,d1_funct_2,t106_zfmisc_1,t48_rcomp_1,t25_topmetr,t106_zfmisc_1,d1_funct_2,t106_zfmisc_1,d1_funct_2,d1_funct_2,t106_zfmisc_1,t12_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,t37_borsuk_6,t14_funct_4,t23_funct_1,t86_funct_3,t91_tmap_1,t37_borsuk_6]), [file(borsuk_6,t83_borsuk_6),interesting(0.00)]). fof(t84_borsuk_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & v1_borsuk_2(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_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_borsuk_2(E,A,B,C) => ! [F] : ( m1_borsuk_2(F,A,B,C) => ! [G] : ( m1_borsuk_2(G,A,C,D) => ! [H] : ( m1_borsuk_2(H,A,C,D) => ( ( r4_borsuk_2(A,B,C,E,F) & r4_borsuk_2(A,C,D,G,H) ) => r4_borsuk_2(A,B,D,k1_borsuk_2(A,B,C,D,E,G),k1_borsuk_2(A,B,C,D,F,H)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_borsuk_2,t83_borsuk_6]), [file(borsuk_6,t84_borsuk_6),interesting(0.00)]). fof(t10_treal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(A,B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(A,B))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k4_topmetr(0,1))) => ! [F] : ( v1_xreal_0(F) => ! [G] : ( v1_xreal_0(G) => ! [H] : ( v1_xreal_0(H) => ( ( E = F & G = C & H = D ) => k8_funct_2(u1_struct_0(k4_topmetr(0,1)),u1_struct_0(k4_topmetr(A,B)),k3_treal_1(A,B,C,D),E) = k2_xcmplx_0(k3_xcmplx_0(k6_xcmplx_0(H,G),F),G) ) ) ) ) ) ) ) ) ) ) ), file(treal_1,t10_treal_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(d9_funct_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k15_funct_3(A,B) <=> ( k1_relat_1(C) = k2_zfmisc_1(k1_relat_1(A),k1_relat_1(B)) & ! [D,E] : ( ( r2_hidden(D,k1_relat_1(A)) & r2_hidden(E,k1_relat_1(B)) ) => k1_funct_1(C,k4_tarski(D,E)) = k4_tarski(k1_funct_1(A,D),k1_funct_1(B,E)) ) ) ) ) ) ) ), file(funct_3,d9_funct_3), [interesting(0.00)]). fof(t12_relset_1,theorem,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) ) ), file(relset_1,t12_relset_1), [interesting(0.00)]). fof(t88_funct_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => k2_relat_1(k15_funct_3(A,B)) = k2_zfmisc_1(k2_relat_1(A),k2_relat_1(B)) ) ) ), file(funct_3,t88_funct_3), [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(t1_treal_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_tarski(k1_rcomp_1(B,C),k1_rcomp_1(A,D)) ) ) ) ) ) ), file(treal_1,t1_treal_1), [interesting(0.00)]). fof(t12_compts_1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( ( B = k1_xboole_0 => ( v6_compts_1(B,A) <=> v2_compts_1(k3_pre_topc(A,B)) ) ) & ( v2_pre_topc(A) => ( B = k1_xboole_0 | ( v6_compts_1(B,A) <=> v2_compts_1(k3_pre_topc(A,B)) ) ) ) ) ) ) ), file(compts_1,t12_compts_1), [interesting(0.00)]). fof(d1_rcomp_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => k1_rcomp_1(A,B) = a_2_0_rcomp_1(A,B) ) ) ), file(rcomp_1,d1_rcomp_1), [interesting(0.00)]). fof(t8_treal_1,theorem, ( k23_borsuk_1 = k1_treal_1(0,1) & k24_borsuk_1 = k2_treal_1(0,1) ), file(treal_1,t8_treal_1), [interesting(0.00)]). fof(t14_treal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ r1_xreal_0(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(k4_topmetr(0,1))) => ! [D] : ( m1_subset_1(D,u1_struct_0(k4_topmetr(0,1))) => ! [E] : ( m1_subset_1(E,u1_struct_0(k4_topmetr(A,B))) => ! [F] : ( m1_subset_1(F,k1_numbers) => ! [G] : ( m1_subset_1(G,k1_numbers) => ! [H] : ( m1_subset_1(H,k1_numbers) => ( ( E = F & G = C & H = D ) => k8_funct_2(u1_struct_0(k4_topmetr(A,B)),u1_struct_0(k4_topmetr(0,1)),k4_treal_1(A,B,C,D),E) = k2_xcmplx_0(k3_xcmplx_0(k7_xcmplx_0(k5_real_1(H,G),k6_xcmplx_0(B,A)),F),k7_xcmplx_0(k6_xcmplx_0(k3_xcmplx_0(B,G),k3_xcmplx_0(A,H)),k6_xcmplx_0(B,A))) ) ) ) ) ) ) ) ) ) ) ), file(treal_1,t14_treal_1), [interesting(0.00)]). fof(t88_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ), file(xcmplx_1,t88_xcmplx_1), [interesting(0.00)]). fof(t90_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => B = k7_xcmplx_0(k3_xcmplx_0(B,A),A) ) ) ) ), file(xcmplx_1,t90_xcmplx_1), [interesting(0.00)]). fof(d7_borsuk_6,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) & m2_relset_1(A,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) ) => ( A = k3_borsuk_6 <=> ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => ( ( r1_xreal_0(B,k6_real_1(1,2)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),A,B) = k3_xcmplx_0(2,B) ) & ( ~ r1_xreal_0(B,k6_real_1(1,2)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),A,B) = 1 ) ) ) ) ) ), file(borsuk_6,d7_borsuk_6), [interesting(0.00)]). fof(d5_seqm_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v5_seqm_3(A) <=> ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) & r2_hidden(C,k1_relat_1(A)) ) => k1_funct_1(A,B) = k1_funct_1(A,C) ) ) ) ), file(seqm_3,d5_seqm_3), [interesting(0.00)]). fof(d8_borsuk_6,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) & m2_relset_1(A,u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr)) ) => ( A = k4_borsuk_6 <=> ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => ( ( r1_xreal_0(B,k6_real_1(1,2)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),A,B) = 0 ) & ( ~ r1_xreal_0(B,k6_real_1(1,2)) => k8_funct_2(u1_struct_0(k5_topmetr),u1_struct_0(k5_topmetr),A,B) = k6_xcmplx_0(k3_xcmplx_0(2,B),1) ) ) ) ) ) ), file(borsuk_6,d8_borsuk_6), [interesting(0.00)]). fof(t12_jgraph_3,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)) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( v1_funct_1(k2_partfun1(u1_struct_0(A),u1_struct_0(B),C,D)) & v1_funct_2(k2_partfun1(u1_struct_0(A),u1_struct_0(B),C,D),u1_struct_0(k3_pre_topc(A,D)),u1_struct_0(B)) & m2_relset_1(k2_partfun1(u1_struct_0(A),u1_struct_0(B),C,D),u1_struct_0(k3_pre_topc(A,D)),u1_struct_0(B)) ) ) ) ) ) ), file(jgraph_3,t12_jgraph_3), [interesting(0.00)]). fof(t10_topmetr,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( ( ~ v3_struct_0(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),u1_struct_0(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(k3_pre_topc(A,C)),u1_struct_0(B)) & m2_relset_1(E,u1_struct_0(k3_pre_topc(A,C)),u1_struct_0(B)) ) => ( ( v5_pre_topc(D,A,B) & E = k2_partfun1(u1_struct_0(A),u1_struct_0(B),D,C) ) => v5_pre_topc(E,k3_pre_topc(A,C),B) ) ) ) ) ) ) ), file(topmetr,t10_topmetr), [interesting(0.00)]). fof(t23_mcart_1,theorem,( ! [A,B,C] : ( r2_hidden(A,k2_zfmisc_1(B,C)) => A = k4_tarski(k1_mcart_1(A),k2_mcart_1(A)) ) ), file(mcart_1,t23_mcart_1), [interesting(0.00)]). fof(d10_borsuk_6,definition,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) => ( A = k6_borsuk_6 <=> ! [B] : ( r2_hidden(B,A) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(k5_topmetr)) & ? [D] : ( m1_subset_1(D,u1_struct_0(k5_topmetr)) & B = k8_borsuk_1(k5_topmetr,k5_topmetr,C,D) & r1_xreal_0(D,k6_xcmplx_0(1,k3_xcmplx_0(2,C))) ) ) ) ) ) ), file(borsuk_6,d10_borsuk_6), [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(t8_mcart_1,theorem,( ! [A] : ( ? [B,C] : A = k4_tarski(B,C) => k4_tarski(k1_mcart_1(A),k2_mcart_1(A)) = A ) ), file(mcart_1,t8_mcart_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(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(d12_borsuk_6,definition,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) => ( A = k8_borsuk_6 <=> ! [B] : ( r2_hidden(B,A) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(k5_topmetr)) & ? [D] : ( m1_subset_1(D,u1_struct_0(k5_topmetr)) & B = k8_borsuk_1(k5_topmetr,k5_topmetr,C,D) & r1_xreal_0(D,k6_xcmplx_0(k3_xcmplx_0(2,C),1)) ) ) ) ) ) ), file(borsuk_6,d12_borsuk_6), [interesting(0.00)]). fof(t15_xboole_1,theorem,( ! [A,B] : ( k2_xboole_0(A,B) = k1_xboole_0 => A = k1_xboole_0 ) ), file(xboole_1,t15_xboole_1), [interesting(0.00)]). fof(d1_struct_0,definition,( ! [A] : ( l1_struct_0(A) => ( v3_struct_0(A) <=> v1_xboole_0(u1_struct_0(A)) ) ) ), file(struct_0,d1_struct_0), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [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(t7_mcart_1,theorem,( ! [A,B] : ( k1_mcart_1(k4_tarski(A,B)) = A & k2_mcart_1(k4_tarski(A,B)) = B ) ), file(mcart_1,t7_mcart_1), [interesting(0.00)]). fof(s7_domain_1,theorem,( m1_subset_1(a_0_0_domain_1,k1_zfmisc_1(f1_s7_domain_1)) ), file(domain_1,s7_domain_1), [interesting(0.00)]). fof(t10_catalg_1,theorem,( ! [A,B] : ( r2_hidden(B,k4_finseq_2(2,A)) <=> ? [C,D] : ( r2_hidden(C,A) & r2_hidden(D,A) & B = k10_finseq_1(C,D) ) ) ), file(catalg_1,t10_catalg_1), [interesting(0.00)]). fof(d1_euclid,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_euclid(A) = k4_finseq_2(A,k1_numbers) ) ), file(euclid,d1_euclid), [interesting(0.00)]). fof(s7_funct_2,theorem, ( ! [A] : ( m1_subset_1(A,f1_s7_funct_2) => ! [B] : ( m1_subset_1(B,f2_s7_funct_2) => ? [C] : ( m1_subset_1(C,f3_s7_funct_2) & p1_s7_funct_2(A,B,C) ) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(f1_s7_funct_2,f2_s7_funct_2),f3_s7_funct_2) & m2_relset_1(A,k2_zfmisc_1(f1_s7_funct_2,f2_s7_funct_2),f3_s7_funct_2) & ! [B] : ( m1_subset_1(B,f1_s7_funct_2) => ! [C] : ( m1_subset_1(C,f2_s7_funct_2) => p1_s7_funct_2(B,C,k1_funct_1(A,k4_tarski(B,C))) ) ) ) ), file(funct_2,s7_funct_2), [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(t85_topreal6,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,u1_struct_0(k6_borsuk_1(k3_topmetr,k3_topmetr)),u1_struct_0(k15_euclid(2))) & m2_relset_1(A,u1_struct_0(k6_borsuk_1(k3_topmetr,k3_topmetr)),u1_struct_0(k15_euclid(2))) ) => ( ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k1_funct_1(A,k4_tarski(B,C)) = k2_finseq_4(k1_numbers,B,C) ) ) => v3_tops_2(A,k6_borsuk_1(k3_topmetr,k3_topmetr),k15_euclid(2)) ) ) ), file(topreal6,t85_topreal6), [interesting(0.00)]). fof(d12_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( C = k9_relat_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E] : ( r2_hidden(E,k1_relat_1(A)) & r2_hidden(E,B) & D = k1_funct_1(A,E) ) ) ) ) ), file(funct_1,d12_funct_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(d14_euclid,definition,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( m1_subset_1(B,k1_numbers) => ( B = k21_euclid(A) <=> ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( A = C => B = k1_funct_1(C,1) ) ) ) ) ) ), file(euclid,d14_euclid), [interesting(0.00)]). fof(t61_finseq_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k10_finseq_1(A,B) <=> ( k3_finseq_1(C) = 2 & k1_funct_1(C,1) = A & k1_funct_1(C,2) = B ) ) ) ), file(finseq_1,t61_finseq_1), [interesting(0.00)]). fof(d15_euclid,definition,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ! [B] : ( m1_subset_1(B,k1_numbers) => ( B = k22_euclid(A) <=> ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( A = C => B = k1_funct_1(C,2) ) ) ) ) ) ), file(euclid,d15_euclid), [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(t55_euclid,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k15_euclid(2))) => ? [B] : ( m1_subset_1(B,k1_numbers) & ? [C] : ( m1_subset_1(C,k1_numbers) & A = k10_finseq_1(B,C) ) ) ) ), file(euclid,t55_euclid), [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(s1_jgraph_2,theorem,( m1_subset_1(a_0_10_jgraph_2,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), file(jgraph_2,s1_jgraph_2), [interesting(0.00)]). fof(t57_jgraph_2,theorem, ( v4_pre_topc(a_0_6_jgraph_2,k15_euclid(2)) & m1_subset_1(a_0_6_jgraph_2,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) & v4_pre_topc(a_0_7_jgraph_2,k15_euclid(2)) & m1_subset_1(a_0_7_jgraph_2,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), file(jgraph_2,t57_jgraph_2), [interesting(0.00)]). fof(t54_jgraph_2,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,0) & ~ r1_xreal_0(C,0) & ~ v2_funct_1(k2_jgraph_2(A,B,C,D)) ) ) ) ) ) ), file(jgraph_2,t54_jgraph_2), [interesting(0.00)]). fof(d2_jgraph_2,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(k15_euclid(2)),u1_struct_0(k15_euclid(2))) & m2_relset_1(E,u1_struct_0(k15_euclid(2)),u1_struct_0(k15_euclid(2))) ) => ( E = k2_jgraph_2(A,B,C,D) <=> ! [F] : ( m1_subset_1(F,u1_struct_0(k15_euclid(2))) => k8_funct_2(u1_struct_0(k15_euclid(2)),u1_struct_0(k15_euclid(2)),E,F) = k23_euclid(k2_xcmplx_0(k3_xcmplx_0(A,k21_euclid(F)),B),k2_xcmplx_0(k3_xcmplx_0(C,k22_euclid(F)),D)) ) ) ) ) ) ) ) ), file(jgraph_2,d2_jgraph_2), [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(t36_jordan1k,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(C,0) & ~ v2_funct_2(k2_jgraph_2(A,B,C,D),u1_struct_0(k15_euclid(2)),u1_struct_0(k15_euclid(2))) ) ) ) ) ) ), file(jordan1k,t36_jordan1k), [interesting(0.00)]). fof(d3_funct_2,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( v2_funct_2(C,A,B) <=> k2_relat_1(C) = B ) ) ), file(funct_2,d3_funct_2), [interesting(0.00)]). fof(t1_msafree3,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( r1_tarski(A,k1_relat_1(B)) & v2_funct_1(B) ) => k10_relat_1(B,k9_relat_1(B,A)) = A ) ) ), file(msafree3,t1_msafree3), [interesting(0.00)]). fof(d12_pre_topc,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)) ) => ( v5_pre_topc(C,A,B) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( v4_pre_topc(D,B) => v4_pre_topc(k5_pre_topc(A,B,C,D),A) ) ) ) ) ) ) ), file(pre_topc,d12_pre_topc), [interesting(0.00)]). fof(t72_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) <=> ( 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))) => ( v4_pre_topc(D,A) <=> v4_pre_topc(k4_pre_topc(A,B,C,D),B) ) ) ) ) ) ) ) ), file(tops_2,t72_tops_2), [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(t35_borsuk_1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_pre_topc(B,A) => r1_tarski(u1_struct_0(B),u1_struct_0(A)) ) ) ), file(borsuk_1,t35_borsuk_1), [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(t43_pre_topc,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_pre_topc(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ( v4_pre_topc(C,B) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & v4_pre_topc(D,A) & k3_xboole_0(D,k2_pre_topc(B)) = C ) ) ) ) ) ), file(pre_topc,t43_pre_topc), [interesting(0.00)]). fof(t10_mcart_1,theorem,( ! [A,B,C] : ( r2_hidden(A,k2_zfmisc_1(B,C)) => ( r2_hidden(k1_mcart_1(A),B) & r2_hidden(k2_mcart_1(A),C) ) ) ), file(mcart_1,t10_mcart_1), [interesting(0.00)]). fof(t31_borsuk_6,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))) => ( m1_subset_1(k1_mcart_1(C),u1_struct_0(A)) & m1_subset_1(k2_mcart_1(C),u1_struct_0(B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,t10_mcart_1]), [file(borsuk_6,t31_borsuk_6),interesting(0.00)]). fof(t56_jgraph_2,theorem, ( v4_pre_topc(a_0_4_jgraph_2,k15_euclid(2)) & m1_subset_1(a_0_4_jgraph_2,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) & v4_pre_topc(a_0_5_jgraph_2,k15_euclid(2)) & m1_subset_1(a_0_5_jgraph_2,k1_zfmisc_1(u1_struct_0(k15_euclid(2)))) ), file(jgraph_2,t56_jgraph_2), [interesting(0.00)]). fof(s10_domain_1,theorem,( a_0_3_domain_1 = k3_xboole_0(a_0_4_domain_1,a_0_5_domain_1) ), file(domain_1,s10_domain_1), [interesting(0.00)]). fof(t35_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))) => ( ( v4_pre_topc(B,A) & v4_pre_topc(C,A) ) => v4_pre_topc(k5_subset_1(u1_struct_0(A),B,C),A) ) ) ) ) ), file(tops_1,t35_tops_1), [interesting(0.00)]). fof(d11_borsuk_6,definition,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr)))) => ( A = k7_borsuk_6 <=> ! [B] : ( r2_hidden(B,A) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(k5_topmetr)) & ? [D] : ( m1_subset_1(D,u1_struct_0(k5_topmetr)) & B = k8_borsuk_1(k5_topmetr,k5_topmetr,C,D) & r1_xreal_0(k6_xcmplx_0(1,k3_xcmplx_0(2,C)),D) & r1_xreal_0(k6_xcmplx_0(k3_xcmplx_0(2,C),1),D) ) ) ) ) ) ), file(borsuk_6,d11_borsuk_6), [interesting(0.00)]). fof(t1_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,A) ) => A = B ) ) ) ), file(xreal_1,t1_xreal_1), [interesting(0.00)]). fof(t219_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(A,k7_xcmplx_0(1,2)) => r1_xreal_0(k6_xcmplx_0(k3_xcmplx_0(2,A),1),0) ) ) ), file(xreal_1,t219_xreal_1), [interesting(0.00)]). fof(t220_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(A,k7_xcmplx_0(1,2)) => r1_xreal_0(0,k6_xcmplx_0(1,k3_xcmplx_0(2,A))) ) ) ), file(xreal_1,t220_xreal_1), [interesting(0.00)]). fof(t6_jordan16,theorem,( ! [A] : ( ( ~ v3_struct_0(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))) => ( r1_tarski(B,C) => m1_pre_topc(k3_pre_topc(A,B),k3_pre_topc(A,C)) ) ) ) ) ), file(jordan16,t6_jordan16), [interesting(0.00)]). fof(t34_tops_2,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_pre_topc(C,A) => ( v4_pre_topc(B,A) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(C))) => ( D = B => v4_pre_topc(D,C) ) ) ) ) ) ) ), file(tops_2,t34_tops_2), [interesting(0.00)]). fof(t9_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] : ( ( ~ v3_struct_0(C) & v2_pre_topc(C) & l1_pre_topc(C) ) => ! [D] : ( ( ~ v3_struct_0(D) & v2_pre_topc(D) & l1_pre_topc(D) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(E,u1_struct_0(A),u1_struct_0(B)) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,u1_struct_0(C),u1_struct_0(B)) & m2_relset_1(F,u1_struct_0(C),u1_struct_0(B)) ) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(D))) => ! [H] : ( m1_subset_1(H,k1_zfmisc_1(u1_struct_0(D))) => ~ ( m1_pre_topc(A,D) & m1_pre_topc(C,D) & G = k2_pre_topc(A) & H = k2_pre_topc(C) & k2_xboole_0(k2_pre_topc(A),k2_pre_topc(C)) = k2_pre_topc(D) & v4_pre_topc(G,D) & v4_pre_topc(H,D) & v5_pre_topc(E,A,B) & v5_pre_topc(F,C,B) & ! [I] : ( r2_hidden(I,k3_xboole_0(k2_pre_topc(A),k2_pre_topc(C))) => k1_funct_1(E,I) = k1_funct_1(F,I) ) & ! [I] : ( ( v1_funct_1(I) & v1_funct_2(I,u1_struct_0(D),u1_struct_0(B)) & m2_relset_1(I,u1_struct_0(D),u1_struct_0(B)) ) => ~ ( I = k1_funct_4(E,F) & v5_pre_topc(I,D,B) ) ) ) ) ) ) ) ) ) ) ) ), file(jgraph_2,t9_jgraph_2), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [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(t23_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(A,k2_xboole_0(B,C)) = k2_xboole_0(k3_xboole_0(A,B),k3_xboole_0(A,C)) ), file(xboole_1,t23_xboole_1), [interesting(0.00)]). fof(t12_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k2_xboole_0(A,B) = B ) ), file(xboole_1,t12_xboole_1), [interesting(0.00)]). fof(t221_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(k7_xcmplx_0(1,2),A) => r1_xreal_0(0,k6_xcmplx_0(k3_xcmplx_0(2,A),1)) ) ) ), file(xreal_1,t221_xreal_1), [interesting(0.00)]). fof(t222_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(k7_xcmplx_0(1,2),A) => r1_xreal_0(k6_xcmplx_0(1,k3_xcmplx_0(2,A)),0) ) ) ), file(xreal_1,t222_xreal_1), [interesting(0.00)]). fof(t36_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))) => ( ( v4_pre_topc(B,A) & v4_pre_topc(C,A) ) => v4_pre_topc(k4_subset_1(u1_struct_0(A),B,C),A) ) ) ) ) ), file(tops_1,t36_tops_1), [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(l94_borsuk_6,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k5_topmetr)) => ! [B] : ( m1_subset_1(B,u1_struct_0(k5_topmetr)) => r2_hidden(k8_borsuk_1(k5_topmetr,k5_topmetr,A,B),u1_struct_0(k6_borsuk_1(k5_topmetr,k5_topmetr))) ) ) ), file(borsuk_6,l94_borsuk_6), [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(t15_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] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_borsuk_2(D,A,B,C) => ( r2_borsuk_2(A,B,C) => r3_borsuk_2(A,B,C,D,D) ) ) ) ) ) ), file(borsuk_2,t15_borsuk_2), [interesting(0.00)]).