fof(t85_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v1_borsuk_1(B,A) & m1_pre_topc(B,A) ) => ! [C] : ( ( v2_borsuk_1(C,B) & m1_borsuk_1(C,B) ) => ( r2_borsuk_1(A,B) => r2_borsuk_1(k16_borsuk_1(A,k20_borsuk_1(A,B,C)),k21_borsuk_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,d21_borsuk_1,t50_borsuk_1,t50_borsuk_1,t21_borsuk_1,t33_zfmisc_1,t78_borsuk_1,t21_funct_2,t33_zfmisc_1,t19_borsuk_1,d2_borsuk_1,d5_borsuk_1,t50_borsuk_1,t24_borsuk_1,t20_borsuk_1,t39_borsuk_1,d10_borsuk_1,t30_borsuk_1,d15_borsuk_1,t67_borsuk_1,t81_borsuk_1,t145_funct_1,t23_borsuk_1,t159_relat_1,t156_relat_1,t1_xboole_1,d21_borsuk_1,t71_borsuk_1,t21_borsuk_1,t21_funct_2,t21_borsuk_1,t21_funct_2,t80_borsuk_1,t79_borsuk_1,t21_borsuk_1,t21_funct_2]), [file(borsuk_1,t85_borsuk_1),interesting(1.00)]). fof(t6_borsuk_1,theorem,( ! [A,B,C] : r1_tarski(k9_relat_1(k2_funcop_1(A,B),C),k1_tarski(B)) ), inference(mizar_proof,[status(thm)],[t19_funcop_1,t144_relat_1,t1_xboole_1]), [file(borsuk_1,t6_borsuk_1),interesting(0.85)]). fof(t82_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => m1_borsuk_1(k15_borsuk_1(A),A) ) ), inference(mizar_proof,[status(thm)],[l78_borsuk_1,d13_borsuk_1]), [file(borsuk_1,t82_borsuk_1),interesting(0.76)]). fof(t30_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,A) ) => ! [C] : ( m2_subset_1(C,k1_zfmisc_1(A),B) => C = k3_funct_2(A,B,k2_borsuk_1(A,B),k6_domain_1(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t29_borsuk_1,d1_tarski,t46_funct_2,d10_xboole_0,d3_tarski,d13_funct_1,d1_tarski,d1_borsuk_1]), [file(borsuk_1,t30_borsuk_1),interesting(0.73)]). fof(l100_borsuk_1,theorem,( k5_pcomps_1(k8_metric_1) = g1_pre_topc(u1_struct_0(k8_metric_1),k4_pcomps_1(k8_metric_1)) ), inference(mizar_proof,[status(thm)],[d6_pcomps_1]), [file(borsuk_1,l100_borsuk_1),interesting(0.72)]). fof(l98_borsuk_1,theorem,( ! [A] : ( l1_pre_topc(A) => m1_pre_topc(g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)),A) ) ), inference(mizar_proof,[status(thm)],[d9_pre_topc,t15_pre_topc,t15_pre_topc]), [file(borsuk_1,l98_borsuk_1),interesting(0.71)]). fof(t5_borsuk_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r1_tarski(A,k10_relat_1(C,B)) => r1_tarski(k9_relat_1(C,A),B) ) ) ), inference(mizar_proof,[status(thm)],[t156_relat_1,t145_funct_1,t1_xboole_1]), [file(borsuk_1,t5_borsuk_1),interesting(0.71)]). fof(t31_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,A) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(B)) => k3_funct_2(A,B,k2_borsuk_1(A,B),C) = k3_tarski(C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t46_funct_2,d1_borsuk_1,d4_tarski,d10_xboole_0,d3_tarski,d4_tarski,t29_borsuk_1,t46_funct_2]), [file(borsuk_1,t31_borsuk_1),interesting(0.71)]). 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)) ) ) ), inference(mizar_proof,[status(thm)],[d9_pre_topc]), [file(borsuk_1,t35_borsuk_1),interesting(0.69)]). fof(t51_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => v1_tops_2(k11_borsuk_1(A,B,C),k6_borsuk_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tops_2,t46_borsuk_1]), [file(borsuk_1,t51_borsuk_1),interesting(0.68)]). fof(t10_borsuk_1,theorem,( ! [A,B,C] : ( r1_tarski(A,k2_zfmisc_1(B,C)) => k1_funct_1(k1_funct_3(k10_funct_3(B,C)),A) = k2_funct_2(k2_zfmisc_1(B,C),C,k10_funct_3(B,C),A) ) ), inference(mizar_proof,[status(thm)],[d6_funct_3,d1_funct_3]), [file(borsuk_1,t10_borsuk_1),interesting(0.66)]). fof(t25_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(B)) => m1_subset_1(k3_tarski(C),k1_zfmisc_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d4_tarski,d4_tarski]), [file(borsuk_1,t25_borsuk_1),interesting(0.66)]). fof(t83_borsuk_1,theorem,( u1_struct_0(k22_borsuk_1) = k1_rcomp_1(0,1) ), inference(mizar_proof,[status(thm)],[l100_borsuk_1,d14_metric_1,d16_borsuk_1,t15_rcomp_1,d10_pre_topc]), [file(borsuk_1,t83_borsuk_1),interesting(0.66)]). fof(t29_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,A) ) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m2_subset_1(D,k1_zfmisc_1(A),B) => ( r2_hidden(C,D) => D = k8_funct_2(A,B,k2_borsuk_1(A,B),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_borsuk_1,t3_xboole_0,d6_eqrel_1]), [file(borsuk_1,t29_borsuk_1),interesting(0.66)]). fof(t67_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( v6_compts_1(D,B) => ! [E] : ( m2_connsp_2(E,k6_borsuk_1(B,A),k7_borsuk_1(B,A,D,k1_struct_0(A,C))) => ? [F] : ( m2_connsp_2(F,B,D) & ? [G] : ( m1_connsp_2(G,A,C) & r1_tarski(k10_borsuk_1(B,A,D,C,F,G),E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,d2_connsp_2,t55_borsuk_1,d1_compts_1,t63_borsuk_1,t62_borsuk_1,t51_borsuk_1,t18_tops_2,t60_borsuk_1,d7_compts_1,t64_borsuk_1,d3_tarski,d1_compts_1,t10_mcart_1,d1_tarski,d1_compts_1,d4_tarski,t116_funct_2,t9_funct_3,t13_borsuk_1,t3_xboole_0,t10_mcart_1,d1_tarski,t10_mcart_1,t23_mcart_1,t106_zfmisc_1,d4_tarski,t1_xboole_1,t18_tops_2,d1_compts_1,t113_zfmisc_1,t3_xboole_1,t2_zfmisc_1,t60_borsuk_1,t26_tops_2,t62_borsuk_1,d1_compts_1,t55_tops_1,d2_connsp_2,t17_finset_1,t60_borsuk_1,t27_tops_2,t61_borsuk_1,t58_borsuk_1,d7_xboole_0,t10_subset_1,d3_xboole_0,t10_mcart_1,d1_tarski,t23_mcart_1,d6_funct_3,d3_xboole_0,t43_funct_2,d1_setfam_1,t55_tops_1,d1_connsp_2,t56_borsuk_1,t2_xboole_1,d2_connsp_2,t113_zfmisc_1,t2_xboole_1]), [file(borsuk_1,t67_borsuk_1),interesting(0.66)]). fof(t9_borsuk_1,theorem,( ! [A,B,C] : ( r1_tarski(A,k2_zfmisc_1(B,C)) => k1_funct_1(k1_funct_3(k9_funct_3(B,C)),A) = k2_funct_2(k2_zfmisc_1(B,C),B,k9_funct_3(B,C),A) ) ), inference(mizar_proof,[status(thm)],[d5_funct_3,d1_funct_3]), [file(borsuk_1,t9_borsuk_1),interesting(0.65)]). fof(t4_borsuk_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => k3_funct_2(A,A,k6_partfun1(A),B) = B ) ), inference(mizar_proof,[status(thm)],[t92_funct_2,t162_funct_1]), [file(borsuk_1,t4_borsuk_1),interesting(0.65)]). fof(t17_borsuk_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => k3_tarski(k5_setfam_1(A,B)) = k3_tarski(a_2_0_borsuk_1(A,B)) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d4_tarski,d4_tarski,d4_tarski,d4_tarski,d10_xboole_0,d3_tarski,d4_tarski,d4_tarski,d4_tarski,d4_tarski]), [file(borsuk_1,t17_borsuk_1),interesting(0.64)]). fof(t41_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => v6_compts_1(k1_struct_0(A,B),A) ) ) ), inference(mizar_proof,[status(thm)],[d7_compts_1,d1_compts_1,t37_zfmisc_1,d4_tarski,t37_zfmisc_1,t37_zfmisc_1,d1_tarski,d4_tarski,t37_zfmisc_1,d1_compts_1]), [file(borsuk_1,t41_borsuk_1),interesting(0.64)]). fof(t39_borsuk_1,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))) => ! [D] : ( m2_connsp_2(D,A,C) => ( r1_tarski(B,C) => m2_connsp_2(D,A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_connsp_2,t1_xboole_1,d2_connsp_2]), [file(borsuk_1,t39_borsuk_1),interesting(0.64)]). fof(t55_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => k1_tops_1(k6_borsuk_1(A,B),C) = k5_setfam_1(u1_struct_0(k6_borsuk_1(A,B)),k11_borsuk_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_tops_1,t54_borsuk_1,t44_tops_1,t52_borsuk_1,t95_zfmisc_1,d10_xboole_0,t51_borsuk_1,t26_tops_2,t53_borsuk_1,t56_tops_1]), [file(borsuk_1,t55_borsuk_1),interesting(0.63)]). fof(t47_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => k1_tops_1(k6_borsuk_1(A,B),k7_borsuk_1(A,B,C,D)) = k7_borsuk_1(A,B,k1_tops_1(A,C),k1_tops_1(B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t54_tops_1,t45_borsuk_1,d4_tarski,t92_zfmisc_1,t1_xboole_1,t138_zfmisc_1,t56_tops_1,t119_zfmisc_1,d10_xboole_0,t51_tops_1,t46_borsuk_1,t44_tops_1,t119_zfmisc_1,t56_tops_1]), [file(borsuk_1,t47_borsuk_1),interesting(0.62)]). fof(t72_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,u1_struct_0(A)) ) => k2_relat_1(k17_borsuk_1(A,B)) = u1_struct_0(k16_borsuk_1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t12_relset_1,d10_xboole_0,d3_tarski,t71_borsuk_1,t6_funct_2]), [file(borsuk_1,t72_borsuk_1),interesting(0.62)]). fof(t26_borsuk_1,theorem,( ! [A,B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(B)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(B)) => k3_tarski(k5_subset_1(B,C,D)) = k3_xboole_0(k3_tarski(C),k3_tarski(D)) ) ) ) ), inference(mizar_proof,[status(thm)],[t97_zfmisc_1,d10_xboole_0,d3_tarski,d3_xboole_0,d4_tarski,d3_xboole_0,d4_tarski,t3_xboole_0,d6_eqrel_1,d3_xboole_0,d4_tarski]), [file(borsuk_1,t26_borsuk_1),interesting(0.60)]). fof(t84_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v1_borsuk_1(B,A) & m1_pre_topc(B,A) ) => ! [C] : ( ( v2_borsuk_1(C,B) & m1_borsuk_1(C,B) ) => ( r1_borsuk_1(A,B) => r1_borsuk_1(k16_borsuk_1(A,k20_borsuk_1(A,B,C)),k21_borsuk_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_borsuk_1,t78_borsuk_1,d19_borsuk_1,t21_funct_2,t76_borsuk_1,t19_borsuk_1,d2_borsuk_1,t20_borsuk_1,t39_borsuk_1,t81_borsuk_1,t159_relat_1,t145_funct_1,d20_borsuk_1,d19_borsuk_1,t71_borsuk_1,t79_borsuk_1,d19_borsuk_1,t76_borsuk_1,t21_funct_2]), [file(borsuk_1,t84_borsuk_1),interesting(0.60)]). fof(t27_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(B)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( D = k3_tarski(C) => k3_subset_1(A,D) = k3_tarski(k3_subset_1(B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_eqrel_1,t18_borsuk_1,d10_xboole_0,d3_tarski,d4_tarski,t50_subset_1,d4_tarski,t3_xboole_0,d6_eqrel_1,t54_subset_1]), [file(borsuk_1,t27_borsuk_1),interesting(0.59)]). fof(t36_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => v5_pre_topc(k3_borsuk_1(B,A,C),B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_borsuk_1,t43_tops_1,d1_connsp_2,d1_connsp_2,t44_tops_1,t13_funcop_1,t6_borsuk_1,t37_zfmisc_1,t1_xboole_1]), [file(borsuk_1,t36_borsuk_1),interesting(0.58)]). fof(t32_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,A) ) => ! [C] : ( m2_subset_1(C,k1_zfmisc_1(A),B) => ? [D] : ( m1_subset_1(D,A) & k8_funct_2(A,B,k2_borsuk_1(A,B),D) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_eqrel_1,t10_subset_1,t29_borsuk_1]), [file(borsuk_1,t32_borsuk_1),interesting(0.58)]). fof(t42_borsuk_1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_pre_topc(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( C = D => ( v6_compts_1(C,A) <=> v6_compts_1(D,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_compts_1,t11_compts_1]), [file(borsuk_1,t42_borsuk_1),interesting(0.53)]). fof(t53_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => r1_tarski(k5_setfam_1(u1_struct_0(k6_borsuk_1(A,B)),k11_borsuk_1(A,B,C)),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d4_tarski]), [file(borsuk_1,t53_borsuk_1),interesting(0.52)]). fof(t48_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_connsp_2(E,A,C) => ! [F] : ( m1_connsp_2(F,B,D) => m1_connsp_2(k7_borsuk_1(A,B,E,F),k6_borsuk_1(A,B),k8_borsuk_1(A,B,C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_connsp_2,t106_zfmisc_1,t47_borsuk_1,d1_connsp_2]), [file(borsuk_1,t48_borsuk_1),interesting(0.48)]). fof(t81_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_borsuk_1(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(k16_borsuk_1(A,B))) => ! [D] : ( m2_connsp_2(D,A,k5_pre_topc(A,k16_borsuk_1(A,B),k17_borsuk_1(A,B),k1_struct_0(k16_borsuk_1(A,B),C))) => m1_connsp_2(k4_pre_topc(A,k16_borsuk_1(A,B),k17_borsuk_1(A,B),D),k16_borsuk_1(A,B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_borsuk_1,t30_borsuk_1,d13_borsuk_1,t31_borsuk_1,t33_borsuk_1,d5_pre_topc,t69_borsuk_1,d5_pre_topc,t156_relat_1,t72_borsuk_1,t156_relat_1,t147_funct_1,t37_zfmisc_1,t54_tops_1,d1_connsp_2]), [file(borsuk_1,t81_borsuk_1),interesting(0.48)]). fof(t49_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ! [E] : ( m2_connsp_2(E,A,C) => ! [F] : ( m2_connsp_2(F,B,D) => m2_connsp_2(k7_borsuk_1(A,B,E,F),k6_borsuk_1(A,B),k7_borsuk_1(A,B,C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_connsp_2,t119_zfmisc_1,t47_borsuk_1,d2_connsp_2]), [file(borsuk_1,t49_borsuk_1),interesting(0.46)]). fof(t73_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => r1_tarski(C,k18_borsuk_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_xboole_1]), [file(borsuk_1,t73_borsuk_1),interesting(0.43)]). fof(t69_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(B)) => ( r2_hidden(k3_tarski(C),u1_pre_topc(A)) <=> r2_hidden(C,u1_pre_topc(k16_borsuk_1(A,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_borsuk_1]), [file(borsuk_1,t69_borsuk_1),interesting(0.43)]). fof(t68_borsuk_1,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))) => ~ ( r2_hidden(B,k15_borsuk_1(A)) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => B != k1_struct_0(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_eqrel_1,t33_eqrel_1]), [file(borsuk_1,t68_borsuk_1),interesting(0.41)]). fof(t14_borsuk_1,theorem,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) => ( ! [E] : ( r2_hidden(E,D) => ( r1_tarski(E,C) & ? [F] : ( m1_subset_1(F,k1_zfmisc_1(A)) & ? [G] : ( m1_subset_1(G,k1_zfmisc_1(B)) & E = k12_mcart_1(A,B,F,G) ) ) ) ) => r1_tarski(k2_zfmisc_1(k3_tarski(k9_relat_1(k1_funct_3(k9_funct_3(A,B)),D)),k1_setfam_1(k9_relat_1(k1_funct_3(k10_funct_3(A,B)),D))),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t10_mcart_1,d4_tarski,d12_funct_1,t9_funct_3,d6_funct_3,d1_funct_3,d12_funct_1,t13_borsuk_1,t13_borsuk_1,d1_setfam_1,t102_zfmisc_1,t11_mcart_1]), [file(borsuk_1,t14_borsuk_1),interesting(0.41)]). fof(t37_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & v5_pre_topc(C,A,B) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => r1_tarski(k5_pre_topc(A,B,C,k1_tops_1(B,D)),k1_tops_1(A,k5_pre_topc(A,B,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_tops_1,t55_tops_2,d3_tarski,t44_tops_1,t178_relat_1,t54_tops_1]), [file(borsuk_1,t37_borsuk_1),interesting(0.35)]). fof(t79_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(k8_funct_2(u1_struct_0(A),u1_struct_0(k16_borsuk_1(A,k18_borsuk_1(A,B,C))),k17_borsuk_1(A,k18_borsuk_1(A,B,C)),D),u1_struct_0(k16_borsuk_1(B,C))) => r2_hidden(D,u1_struct_0(B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_borsuk_1,d1_borsuk_1]), [file(borsuk_1,t79_borsuk_1),interesting(0.31)]). fof(t70_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r2_hidden(C,k8_funct_2(u1_struct_0(A),u1_struct_0(k16_borsuk_1(A,B)),k17_borsuk_1(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_borsuk_1]), [file(borsuk_1,t70_borsuk_1),interesting(0.28)]). fof(t77_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ~ r2_hidden(D,u1_struct_0(B)) => k8_funct_2(u1_struct_0(A),u1_struct_0(k16_borsuk_1(A,k18_borsuk_1(A,B,C))),k17_borsuk_1(A,k18_borsuk_1(A,B,C)),D) = k1_struct_0(A,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t75_borsuk_1,d1_tarski,t29_borsuk_1]), [file(borsuk_1,t77_borsuk_1),interesting(0.26)]). fof(t78_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k8_funct_2(u1_struct_0(A),u1_struct_0(k16_borsuk_1(A,k18_borsuk_1(A,B,C))),k17_borsuk_1(A,k18_borsuk_1(A,B,C)),D) = k8_funct_2(u1_struct_0(A),u1_struct_0(k16_borsuk_1(A,k18_borsuk_1(A,B,C))),k17_borsuk_1(A,k18_borsuk_1(A,B,C)),E) => ( r2_hidden(D,u1_struct_0(B)) | D = E ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t77_borsuk_1,d1_borsuk_1,d1_tarski]), [file(borsuk_1,t78_borsuk_1),interesting(0.22)]). fof(t15_borsuk_1,theorem,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(A,B)))) => ( ! [E] : ( r2_hidden(E,D) => ( r1_tarski(E,C) & ? [F] : ( m1_subset_1(F,k1_zfmisc_1(A)) & ? [G] : ( m1_subset_1(G,k1_zfmisc_1(B)) & E = k12_mcart_1(A,B,F,G) ) ) ) ) => r1_tarski(k2_zfmisc_1(k1_setfam_1(k9_relat_1(k1_funct_3(k9_funct_3(A,B)),D)),k3_tarski(k9_relat_1(k1_funct_3(k10_funct_3(A,B)),D))),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t10_mcart_1,d4_tarski,d12_funct_1,t9_funct_3,d5_funct_3,d1_funct_3,d12_funct_1,t13_borsuk_1,t13_borsuk_1,d1_setfam_1,t102_zfmisc_1,t11_mcart_1]), [file(borsuk_1,t15_borsuk_1),interesting(0.21)]). fof(t62_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(B))) => ( r1_compts_1(k6_borsuk_1(A,B),C,k7_borsuk_1(A,B,D,E)) => ( ( E != k1_xboole_0 => r1_compts_1(A,k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(A),k12_borsuk_1(A,B),C),D) ) & ( D != k1_xboole_0 => r1_compts_1(B,k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(B),k13_borsuk_1(A,B),C),E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,d1_compts_1,t10_subset_1,d3_tarski,d1_compts_1,t106_zfmisc_1,d4_tarski,d1_funct_3,d5_funct_3,t9_borsuk_1,d12_funct_1,t106_zfmisc_1,d5_funct_3,d5_funct_3,d12_funct_1,d4_tarski,t10_subset_1,d3_tarski,d1_compts_1,t106_zfmisc_1,d4_tarski,d1_funct_3,d6_funct_3,t10_borsuk_1,d12_funct_1,t106_zfmisc_1,d6_funct_3,d6_funct_3,d12_funct_1,d4_tarski]), [file(borsuk_1,t62_borsuk_1),interesting(0.20)]). fof(t38_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(B),u1_struct_0(A)) & v5_pre_topc(D,B,A) & m2_relset_1(D,u1_struct_0(B),u1_struct_0(A)) ) => ! [E] : ( m1_connsp_2(E,A,C) => m2_connsp_2(k5_pre_topc(B,A,D,E),B,k5_pre_topc(B,A,D,k1_struct_0(A,C))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_connsp_2,t37_zfmisc_1,t178_relat_1,t37_borsuk_1,t1_xboole_1,d2_connsp_2]), [file(borsuk_1,t38_borsuk_1),interesting(0.17)]). fof(t76_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,u1_struct_0(B)) => k8_funct_2(u1_struct_0(A),u1_struct_0(k16_borsuk_1(A,k18_borsuk_1(A,B,C))),k17_borsuk_1(A,k18_borsuk_1(A,B,C)),D) = k1_funct_1(k17_borsuk_1(B,C),D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_xboole_1,d1_borsuk_1,t29_borsuk_1]), [file(borsuk_1,t76_borsuk_1),interesting(0.15)]). fof(t58_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ! [D] : ~ ( r2_hidden(D,k2_funct_2(k1_pcomps_1(u1_struct_0(k6_borsuk_1(A,B))),k1_pcomps_1(u1_struct_0(B)),k13_borsuk_1(A,B),C)) & ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ~ ( r2_hidden(E,C) & D = k2_funct_2(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(B),k10_funct_3(u1_struct_0(A),u1_struct_0(B)),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,d12_funct_1,t10_borsuk_1]), [file(borsuk_1,t58_borsuk_1),interesting(0.14)]). fof(t59_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ( v3_pre_topc(C,k6_borsuk_1(A,B)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(B))) => ( ( D = k2_funct_2(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(A),k9_funct_3(u1_struct_0(A),u1_struct_0(B)),C) => v3_pre_topc(D,A) ) & ( E = k2_funct_2(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(B),k10_funct_3(u1_struct_0(A),u1_struct_0(B)),C) => v3_pre_topc(E,B) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t45_borsuk_1,d5_borsuk_1,d1_tops_2,t116_funct_2,d1_funct_2,t8_funct_3,t12_borsuk_1,t149_relat_1,t52_tops_1,t16_borsuk_1,t26_tops_2,d1_tops_2,t116_funct_2,d1_funct_2,t8_funct_3,t12_borsuk_1,t149_relat_1,t52_tops_1,t16_borsuk_1,t26_tops_2]), [file(borsuk_1,t59_borsuk_1),interesting(0.09)]). fof(t74_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r2_hidden(D,k18_borsuk_1(A,B,C)) & ~ r2_hidden(D,C) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r2_hidden(E,k2_pre_topc(B)) & D = k1_struct_0(A,E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_xboole_0]), [file(borsuk_1,t74_borsuk_1),interesting(0.05)]). fof(t57_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ! [D] : ~ ( r2_hidden(D,k2_funct_2(k1_pcomps_1(u1_struct_0(k6_borsuk_1(A,B))),k1_pcomps_1(u1_struct_0(A)),k12_borsuk_1(A,B),C)) & ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ~ ( r2_hidden(E,C) & D = k2_funct_2(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(B)),u1_struct_0(A),k9_funct_3(u1_struct_0(A),u1_struct_0(B)),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,d12_funct_1,t9_borsuk_1]), [file(borsuk_1,t57_borsuk_1),interesting(0.05)]). fof(t65_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( k7_borsuk_1(A,B,C,D) != k1_xboole_0 => ( k8_funct_2(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))),k1_pcomps_1(u1_struct_0(A)),k12_borsuk_1(A,B),k7_borsuk_1(A,B,C,D)) = C & k8_funct_2(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))),k1_pcomps_1(u1_struct_0(B)),k13_borsuk_1(A,B),k7_borsuk_1(A,B,C,D)) = D ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_borsuk_1]), [file(borsuk_1,t65_borsuk_1),interesting(0.03)]). fof(d9_pre_topc,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( l1_pre_topc(B) => ( m1_pre_topc(B,A) <=> ( r1_tarski(k2_pre_topc(B),k2_pre_topc(A)) & ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(C,u1_pre_topc(B)) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & r2_hidden(D,u1_pre_topc(A)) & C = k3_xboole_0(D,k2_pre_topc(B)) ) ) ) ) ) ) ) ), file(pre_topc,d9_pre_topc), [interesting(0.00)]). fof(t15_pre_topc,theorem,( ! [A] : ( l1_struct_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => k5_subset_1(u1_struct_0(A),B,k2_pre_topc(A)) = B ) ) ), file(pre_topc,t15_pre_topc), [interesting(0.00)]). fof(t11_borsuk_1,theorem,( $true ), file(borsuk_1,t11_borsuk_1), [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(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(d4_tarski,definition,( ! [A,B] : ( B = k3_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(C,D) & r2_hidden(D,A) ) ) ) ), file(tarski,d4_tarski), [interesting(0.00)]). fof(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(t9_funct_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => k1_funct_1(k1_funct_3(A),k1_xboole_0) = k1_xboole_0 ) ), file(funct_3,t9_funct_3), [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(d1_funct_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( B = k1_funct_3(A) <=> ( k1_relat_1(B) = k1_zfmisc_1(k1_relat_1(A)) & ! [C] : ( r1_tarski(C,k1_relat_1(A)) => k1_funct_1(B,C) = k9_relat_1(A,C) ) ) ) ) ) ), file(funct_3,d1_funct_3), [interesting(0.00)]). fof(t113_zfmisc_1,theorem,( ! [A,B] : ( k2_zfmisc_1(A,B) = k1_xboole_0 <=> ( A = k1_xboole_0 | B = k1_xboole_0 ) ) ), file(zfmisc_1,t113_zfmisc_1), [interesting(0.00)]). fof(t3_xboole_1,theorem,( ! [A] : ( r1_tarski(A,k1_xboole_0) => A = k1_xboole_0 ) ), file(xboole_1,t3_xboole_1), [interesting(0.00)]). fof(t115_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ~ ( r2_hidden(E,k2_funct_2(A,B,D,C)) & ! [F] : ~ ( r2_hidden(F,A) & r2_hidden(F,C) & E = k1_funct_1(D,F) ) ) ) ), file(funct_2,t115_funct_2), [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(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(t43_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( B != k1_xboole_0 => ! [E] : ( ? [F] : ( r2_hidden(F,A) & r2_hidden(F,C) & E = k1_funct_1(D,F) ) => r2_hidden(E,k9_relat_1(D,C)) ) ) ) ), file(funct_2,t43_funct_2), [interesting(0.00)]). fof(t2_tarski,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), [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(t12_borsuk_1,theorem,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(B)) => ( k12_mcart_1(A,B,C,D) != k1_xboole_0 => ( k2_funct_2(k2_zfmisc_1(A,B),A,k9_funct_3(A,B),k12_mcart_1(A,B,C,D)) = C & k2_funct_2(k2_zfmisc_1(A,B),B,k10_funct_3(A,B),k12_mcart_1(A,B,C,D)) = D ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_zfmisc_1,t3_xboole_1,t115_funct_2,t23_mcart_1,t10_mcart_1,t10_mcart_1,d5_funct_3,d3_tarski,t106_zfmisc_1,d5_funct_3,t43_funct_2,t2_tarski,t115_funct_2,t23_mcart_1,t10_mcart_1,t10_mcart_1,d6_funct_3,d3_tarski,t106_zfmisc_1,d6_funct_3,t43_funct_2,t2_tarski]), [file(borsuk_1,t12_borsuk_1),interesting(0.00)]). fof(t13_borsuk_1,theorem,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(B)) => ( k12_mcart_1(A,B,C,D) != k1_xboole_0 => ( k1_funct_1(k1_funct_3(k9_funct_3(A,B)),k12_mcart_1(A,B,C,D)) = C & k1_funct_1(k1_funct_3(k10_funct_3(A,B)),k12_mcart_1(A,B,C,D)) = D ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_borsuk_1,t12_borsuk_1,t10_borsuk_1,t12_borsuk_1]), [file(borsuk_1,t13_borsuk_1),interesting(0.00)]). fof(d1_setfam_1,definition,( ! [A,B] : ( ( A != k1_xboole_0 => ( B = k1_setfam_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ! [D] : ( r2_hidden(D,A) => r2_hidden(C,D) ) ) ) ) & ( A = k1_xboole_0 => ( B = k1_setfam_1(A) <=> B = k1_xboole_0 ) ) ) ), file(setfam_1,d1_setfam_1), [interesting(0.00)]). fof(t102_zfmisc_1,theorem,( ! [A,B,C] : ~ ( r2_hidden(A,k2_zfmisc_1(B,C)) & ! [D,E] : k4_tarski(D,E) != A ) ), file(zfmisc_1,t102_zfmisc_1), [interesting(0.00)]). fof(t11_mcart_1,theorem,( ! [A,B,C] : ( ( r2_hidden(k1_mcart_1(A),B) & r2_hidden(k2_mcart_1(A),C) ) => ( ! [D,E] : A != k4_tarski(D,E) | r2_hidden(A,k2_zfmisc_1(B,C)) ) ) ), file(mcart_1,t11_mcart_1), [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(t1_borsuk_1,theorem,( $true ), file(borsuk_1,t1_borsuk_1), [interesting(0.00)]). fof(t22_borsuk_1,theorem,( $true ), file(borsuk_1,t22_borsuk_1), [interesting(0.00)]). fof(t97_zfmisc_1,theorem,( ! [A,B] : r1_tarski(k3_tarski(k3_xboole_0(A,B)),k3_xboole_0(k3_tarski(A),k3_tarski(B))) ), file(zfmisc_1,t97_zfmisc_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(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(d6_eqrel_1,definition,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => ( ( A != k1_xboole_0 => ( m1_eqrel_1(B,A) <=> ( k5_setfam_1(A,B) = A & ! [C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ( r2_hidden(C,B) => ( C != k1_xboole_0 & ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ~ ( r2_hidden(D,B) & C != D & ~ r1_xboole_0(C,D) ) ) ) ) ) ) ) ) & ( A = k1_xboole_0 => ( m1_eqrel_1(B,A) <=> B = k1_xboole_0 ) ) ) ) ), file(eqrel_1,d6_eqrel_1), [interesting(0.00)]). fof(t54_subset_1,theorem,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ~ ( r2_hidden(B,k3_subset_1(A,C)) & r2_hidden(B,C) ) ) ), file(subset_1,t54_subset_1), [interesting(0.00)]). fof(t50_subset_1,theorem,( ! [A] : ( A != k1_xboole_0 => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ! [C] : ( m1_subset_1(C,A) => ( ~ r2_hidden(C,B) => r2_hidden(C,k3_subset_1(A,B)) ) ) ) ) ), file(subset_1,t50_subset_1), [interesting(0.00)]). fof(t18_borsuk_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => ( k5_setfam_1(A,B) = A => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(B)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( D = k3_tarski(C) => r1_tarski(k3_subset_1(A,D),k3_tarski(k3_subset_1(B,C))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d4_tarski,t54_subset_1,d4_tarski,t50_subset_1,d4_tarski]), [file(borsuk_1,t18_borsuk_1),interesting(0.00)]). fof(t28_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v3_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,A,A) & m2_relset_1(B,A,A) ) => ~ v1_xboole_0(k8_eqrel_1(A,B)) ) ) ), file(borsuk_1,t28_borsuk_1), [interesting(0.00)]). fof(t2_borsuk_1,theorem,( $true ), file(borsuk_1,t2_borsuk_1), [interesting(0.00)]). fof(t34_borsuk_1,theorem,( $true ), file(borsuk_1,t34_borsuk_1), [interesting(0.00)]). fof(d2_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( v5_pre_topc(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_connsp_2(E,B,k8_funct_2(u1_struct_0(A),u1_struct_0(B),C,D)) => ? [F] : ( m1_connsp_2(F,A,D) & r1_tarski(k4_pre_topc(A,B,C,F),E) ) ) ) ) ) ) ) ), file(borsuk_1,d2_borsuk_1), [interesting(0.00)]). fof(t43_tops_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => k1_tops_1(A,k2_pre_topc(A)) = k2_pre_topc(A) ) ), file(tops_1,t43_tops_1), [interesting(0.00)]). fof(d1_connsp_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,k1_zfmisc_1(u1_struct_0(A))) => ( m1_connsp_2(C,A,B) <=> r2_hidden(B,k1_tops_1(A,C)) ) ) ) ) ), file(connsp_2,d1_connsp_2), [interesting(0.00)]). fof(t44_tops_1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => r1_tarski(k1_tops_1(A,B),B) ) ) ), file(tops_1,t44_tops_1), [interesting(0.00)]). fof(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [interesting(0.00)]). fof(t19_funcop_1,theorem,( ! [A,B] : ( k1_relat_1(k2_funcop_1(A,B)) = A & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ), file(funcop_1,t19_funcop_1), [interesting(0.00)]). fof(t144_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => r1_tarski(k9_relat_1(B,A),k2_relat_1(B)) ) ), file(relat_1,t144_relat_1), [interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(t178_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r1_tarski(A,B) => r1_tarski(k10_relat_1(C,A),k10_relat_1(C,B)) ) ) ), file(relat_1,t178_relat_1), [interesting(0.00)]). fof(t51_tops_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => v3_pre_topc(k1_tops_1(A,B),A) ) ) ), file(tops_1,t51_tops_1), [interesting(0.00)]). fof(t55_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)) ) => ( v5_pre_topc(C,A,B) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( v3_pre_topc(D,B) => v3_pre_topc(k5_pre_topc(A,B,C,D),A) ) ) ) ) ) ) ), file(tops_2,t55_tops_2), [interesting(0.00)]). fof(t54_tops_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B,C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(B,k1_tops_1(A,C)) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & v3_pre_topc(D,A) & r1_tarski(D,C) & r2_hidden(B,D) ) ) ) ) ), file(tops_1,t54_tops_1), [interesting(0.00)]). fof(d2_connsp_2,definition,( ! [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))) => ( m2_connsp_2(C,A,B) <=> r1_tarski(B,k1_tops_1(A,C)) ) ) ) ) ), file(connsp_2,d2_connsp_2), [interesting(0.00)]). fof(t3_borsuk_1,theorem,( $true ), file(borsuk_1,t3_borsuk_1), [interesting(0.00)]). fof(t40_borsuk_1,theorem,( $true ), file(borsuk_1,t40_borsuk_1), [interesting(0.00)]). fof(d7_compts_1,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v6_compts_1(B,A) <=> ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ~ ( r1_compts_1(A,C,B) & v1_tops_2(C,A) & ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ~ ( r1_tarski(D,C) & r1_compts_1(A,D,B) & v1_finset_1(D) ) ) ) ) ) ) ) ), file(compts_1,d7_compts_1), [interesting(0.00)]). fof(d1_compts_1,definition,( ! [A] : ( l1_struct_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r1_compts_1(A,B,C) <=> r1_tarski(C,k5_setfam_1(u1_struct_0(A),B)) ) ) ) ) ), file(compts_1,d1_compts_1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t11_compts_1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_pre_topc(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r1_tarski(C,k2_pre_topc(B)) => ( v6_compts_1(C,A) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( D = C => v6_compts_1(D,B) ) ) ) ) ) ) ) ), file(compts_1,t11_compts_1), [interesting(0.00)]). fof(t43_borsuk_1,theorem,( $true ), file(borsuk_1,t43_borsuk_1), [interesting(0.00)]). fof(t44_borsuk_1,theorem,( $true ), file(borsuk_1,t44_borsuk_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(d5_pre_topc,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v3_pre_topc(B,A) <=> r2_hidden(B,u1_pre_topc(A)) ) ) ) ), file(pre_topc,d5_pre_topc), [interesting(0.00)]). fof(t45_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ( v3_pre_topc(C,k6_borsuk_1(A,B)) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) & C = k5_setfam_1(u1_struct_0(k6_borsuk_1(A,B)),D) & ! [E] : ~ ( r2_hidden(E,D) & ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(B))) => ~ ( E = k12_mcart_1(u1_struct_0(A),u1_struct_0(B),F,G) & v3_pre_topc(F,A) & v3_pre_topc(G,B) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,d5_pre_topc,d5_pre_topc,d3_tarski,d5_pre_topc,d5_pre_topc]), [file(borsuk_1,t45_borsuk_1),interesting(0.00)]). fof(t92_zfmisc_1,theorem,( ! [A,B] : ( r2_hidden(A,B) => r1_tarski(A,k3_tarski(B)) ) ), file(zfmisc_1,t92_zfmisc_1), [interesting(0.00)]). fof(t138_zfmisc_1,theorem,( ! [A,B,C,D] : ( r1_tarski(k2_zfmisc_1(A,B),k2_zfmisc_1(C,D)) => ( k2_zfmisc_1(A,B) = k1_xboole_0 | ( r1_tarski(A,C) & r1_tarski(B,D) ) ) ) ), file(zfmisc_1,t138_zfmisc_1), [interesting(0.00)]). fof(t56_tops_1,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( ( v3_pre_topc(B,A) & r1_tarski(B,C) ) => r1_tarski(B,k1_tops_1(A,C)) ) ) ) ) ), file(tops_1,t56_tops_1), [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(t31_zfmisc_1,theorem,( ! [A] : k3_tarski(k1_tarski(A)) = A ), file(zfmisc_1,t31_zfmisc_1), [interesting(0.00)]). fof(t46_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( ( v3_pre_topc(C,A) & v3_pre_topc(D,B) ) => v3_pre_topc(k7_borsuk_1(A,B,C,D),k6_borsuk_1(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_zfmisc_1,d1_tarski,t45_borsuk_1]), [file(borsuk_1,t46_borsuk_1),interesting(0.00)]). fof(t156_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( r1_tarski(A,B) => r1_tarski(k9_relat_1(C,A),k9_relat_1(C,B)) ) ) ), file(relat_1,t156_relat_1), [interesting(0.00)]). fof(t145_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => r1_tarski(k9_relat_1(B,k10_relat_1(B,A)),A) ) ), file(funct_1,t145_funct_1), [interesting(0.00)]). fof(t66_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ( k1_funct_1(k12_borsuk_1(A,B),k1_xboole_0) = k1_xboole_0 & k1_funct_1(k13_borsuk_1(A,B),k1_xboole_0) = k1_xboole_0 ) ) ) ), inference(mizar_proof,[status(thm)],[t9_funct_3]), [file(borsuk_1,t66_borsuk_1),interesting(0.00)]). fof(d1_borsuk_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( C = k2_borsuk_1(A,B) <=> ! [D] : ( m1_subset_1(D,A) => r2_hidden(D,k8_funct_2(A,B,C,D)) ) ) ) ) ) ), file(borsuk_1,d1_borsuk_1), [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(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(t7_borsuk_1,theorem,( $true ), file(borsuk_1,t7_borsuk_1), [interesting(0.00)]). fof(d5_eqrel_1,definition,( ! [A,B] : ( ( v3_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,A,A) & m2_relset_1(B,A,A) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A))) => ( C = k7_eqrel_1(A,B) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( r2_hidden(D,C) <=> ? [E] : ( r2_hidden(E,A) & D = k6_eqrel_1(A,B,E) ) ) ) ) ) ) ), file(eqrel_1,d5_eqrel_1), [interesting(0.00)]). fof(t33_eqrel_1,theorem,( ! [A,B] : ( r2_hidden(B,A) => k6_eqrel_1(A,k6_partfun1(A),B) = k1_tarski(B) ) ), file(eqrel_1,t33_eqrel_1), [interesting(0.00)]). fof(t56_zfmisc_1,theorem,( ! [A,B] : ( ~ r2_hidden(A,B) => r1_xboole_0(k1_tarski(A),B) ) ), file(zfmisc_1,t56_zfmisc_1), [interesting(0.00)]). fof(l78_borsuk_1,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))) => ( r2_hidden(B,k15_borsuk_1(A)) => ! [C] : ( m2_connsp_2(C,A,B) => ? [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) & v3_pre_topc(D,A) & r1_tarski(B,D) & r1_tarski(D,C) & ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(E,k15_borsuk_1(A)) => ( r1_xboole_0(E,D) | r1_tarski(E,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_tops_1,d2_connsp_2,t44_tops_1,t68_borsuk_1,t56_zfmisc_1,t37_zfmisc_1]), [file(borsuk_1,l78_borsuk_1),interesting(0.00)]). fof(d13_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,u1_struct_0(A)) ) => ( m1_borsuk_1(B,A) <=> ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(C,B) => ! [D] : ( m2_connsp_2(D,A,C) => ? [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) & v3_pre_topc(E,A) & r1_tarski(C,E) & r1_tarski(E,D) & ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(F,B) => ( r1_xboole_0(F,E) | r1_tarski(F,E) ) ) ) ) ) ) ) ) ) ) ), file(borsuk_1,d13_borsuk_1), [interesting(0.00)]). fof(d6_pcomps_1,definition,( ! [A] : ( l1_metric_1(A) => k5_pcomps_1(A) = g1_pre_topc(u1_struct_0(A),k4_pcomps_1(A)) ) ), file(pcomps_1,d6_pcomps_1), [interesting(0.00)]). fof(d14_metric_1,definition,( k8_metric_1 = g1_metric_1(k1_numbers,k7_metric_1) ), file(metric_1,d14_metric_1), [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(t15_rcomp_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ~ ( ~ r1_xreal_0(B,A) & k2_rcomp_1(A,B) = k1_xboole_0 ) & ( r1_xreal_0(A,B) => ( r2_hidden(A,k1_rcomp_1(A,B)) & r2_hidden(B,k1_rcomp_1(A,B)) ) ) & r1_tarski(k2_rcomp_1(A,B),k1_rcomp_1(A,B)) ) ) ) ), file(rcomp_1,t15_rcomp_1), [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(d20_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ( r1_borsuk_1(A,B) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & v5_pre_topc(C,A,B) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) & v3_borsuk_1(C,A,B) ) ) ) ) ), file(borsuk_1,d20_borsuk_1), [interesting(0.00)]). fof(t75_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ~ r2_hidden(D,u1_struct_0(B)) => r2_hidden(k1_struct_0(A,D),k18_borsuk_1(A,B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_eqrel_1,d4_tarski,d2_xboole_0,d1_tarski]), [file(borsuk_1,t75_borsuk_1),interesting(0.00)]). fof(d19_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( v3_borsuk_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,u1_struct_0(B)) => k8_funct_2(u1_struct_0(A),u1_struct_0(B),C,D) = D ) ) ) ) ) ) ), file(borsuk_1,d19_borsuk_1), [interesting(0.00)]). fof(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(s1_funct_2,theorem, ( ! [A] : ~ ( r2_hidden(A,f1_s1_funct_2) & ! [B] : ~ ( r2_hidden(B,f2_s1_funct_2) & p1_s1_funct_2(A,B) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,f1_s1_funct_2,f2_s1_funct_2) & m2_relset_1(A,f1_s1_funct_2,f2_s1_funct_2) & ! [B] : ( r2_hidden(B,f1_s1_funct_2) => p1_s1_funct_2(B,k1_funct_1(A,B)) ) ) ), file(funct_2,s1_funct_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(t19_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,C) & m2_relset_1(E,A,C) ) => ~ ( ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ( k8_funct_2(A,B,D,F) = k8_funct_2(A,B,D,G) => k8_funct_2(A,C,E,F) = k8_funct_2(A,C,E,G) ) ) ) & ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,C) & m2_relset_1(F,B,C) ) => k7_funct_2(A,B,C,D,F) != E ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s1_funct_2,t21_funct_2,t113_funct_2]), [file(borsuk_1,t19_borsuk_1),interesting(0.00)]). fof(t53_funct_2,theorem,( ! [A,B,C,D,E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,C) & m2_relset_1(F,B,C) ) => ~ ( ( C = k1_xboole_0 => B = k1_xboole_0 ) & ( B = k1_xboole_0 => A = k1_xboole_0 ) & ~ r1_tarski(k3_funct_2(A,B,E,D),k3_funct_2(A,C,k1_partfun1(A,B,B,C,E,F),k2_funct_2(B,C,F,D))) ) ) ) ), file(funct_2,t53_funct_2), [interesting(0.00)]). fof(t13_setwiseo,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,B,A) & m2_relset_1(C,B,A) ) => ! [D] : ( m1_subset_1(D,B) => k2_funct_2(B,A,C,k1_tarski(D)) = k1_tarski(k8_funct_2(B,A,C,D)) ) ) ) ) ), file(setwiseo,t13_setwiseo), [interesting(0.00)]). fof(t20_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,B) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,C) & m2_relset_1(F,B,C) ) => r1_tarski(k3_funct_2(A,B,E,k6_domain_1(B,D)),k3_funct_2(A,C,k7_funct_2(A,B,C,E,F),k6_domain_1(C,k8_funct_2(B,C,F,D)))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_funct_2,t13_setwiseo]), [file(borsuk_1,t20_borsuk_1),interesting(0.00)]). fof(d10_borsuk_1,definition,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_eqrel_1(B,u1_struct_0(A)) => ! [C] : ( ( v1_pre_topc(C) & v2_pre_topc(C) & l1_pre_topc(C) ) => ( C = k16_borsuk_1(A,B) <=> ( u1_struct_0(C) = B & u1_pre_topc(C) = a_2_2_borsuk_1(A,B) ) ) ) ) ) ), file(borsuk_1,d10_borsuk_1), [interesting(0.00)]). fof(t46_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( B != k1_xboole_0 => ! [E] : ( r2_hidden(E,k10_relat_1(D,C)) <=> ( r2_hidden(E,A) & r2_hidden(k1_funct_1(D,E),C) ) ) ) ) ), file(funct_2,t46_funct_2), [interesting(0.00)]). fof(d13_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( C = k10_relat_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,k1_relat_1(A)) & r2_hidden(k1_funct_1(A,D),B) ) ) ) ) ), file(funct_1,d13_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(t146_funct_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => r1_tarski(A,k10_relat_1(B,k9_relat_1(B,A))) ) ) ), file(funct_1,t146_funct_1), [interesting(0.00)]). fof(t116_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ~ ( r2_hidden(E,k2_funct_2(A,B,D,C)) & ! [F] : ( m1_subset_1(F,A) => ~ ( r2_hidden(F,C) & E = k1_funct_1(D,F) ) ) ) ) ), file(funct_2,t116_funct_2), [interesting(0.00)]). fof(t33_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,A) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ( ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( r2_hidden(D,B) => ( r1_xboole_0(D,C) | r1_tarski(D,C) ) ) ) => C = k3_funct_2(A,B,k2_borsuk_1(A,B),k2_funct_2(A,B,k2_borsuk_1(A,B),C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t146_funct_1,d10_xboole_0,d3_tarski,d13_funct_1,t116_funct_2,d3_tarski,d1_borsuk_1,t3_xboole_0,d1_borsuk_1]), [file(borsuk_1,t33_borsuk_1),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(t10_subset_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ~ ( B != k1_xboole_0 & ! [C] : ( m1_subset_1(C,A) => ~ r2_hidden(C,B) ) ) ) ), file(subset_1,t10_subset_1), [interesting(0.00)]). fof(t71_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & m1_eqrel_1(B,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k16_borsuk_1(A,B))) => ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & k8_funct_2(u1_struct_0(A),u1_struct_0(k16_borsuk_1(A,B)),k17_borsuk_1(A,B),D) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_borsuk_1,t32_borsuk_1]), [file(borsuk_1,t71_borsuk_1),interesting(0.00)]). fof(t6_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( r2_hidden(C,A) => ( B = k1_xboole_0 | r2_hidden(k1_funct_1(D,C),k2_relat_1(D)) ) ) ) ), file(funct_2,t6_funct_2), [interesting(0.00)]). fof(t147_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(A,k2_relat_1(B)) => k9_relat_1(B,k10_relat_1(B,A)) = A ) ) ), file(funct_1,t147_funct_1), [interesting(0.00)]). fof(t159_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ! [C] : ( v1_relat_1(C) => k9_relat_1(k5_relat_1(B,C),A) = k9_relat_1(C,k9_relat_1(B,A)) ) ) ), file(relat_1,t159_relat_1), [interesting(0.00)]). fof(d21_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ( r2_borsuk_1(A,B) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(k6_borsuk_1(A,k22_borsuk_1)),u1_struct_0(A)) & v5_pre_topc(C,k6_borsuk_1(A,k22_borsuk_1),A) & m2_relset_1(C,u1_struct_0(k6_borsuk_1(A,k22_borsuk_1)),u1_struct_0(A)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( k8_funct_2(u1_struct_0(k6_borsuk_1(A,k22_borsuk_1)),u1_struct_0(A),C,k8_borsuk_1(A,k22_borsuk_1,D,k23_borsuk_1)) = D & r2_hidden(k8_funct_2(u1_struct_0(k6_borsuk_1(A,k22_borsuk_1)),u1_struct_0(A),C,k8_borsuk_1(A,k22_borsuk_1,D,k24_borsuk_1)),u1_struct_0(B)) & ( r2_hidden(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(k22_borsuk_1)) => k8_funct_2(u1_struct_0(k6_borsuk_1(A,k22_borsuk_1)),u1_struct_0(A),C,k8_borsuk_1(A,k22_borsuk_1,D,E)) = D ) ) ) ) ) ) ) ) ), file(borsuk_1,d21_borsuk_1), [interesting(0.00)]). fof(t9_domain_1,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ~ ( r2_hidden(A,k2_zfmisc_1(B,C)) & ! [D] : ( m1_subset_1(D,B) => ! [E] : ( m1_subset_1(E,C) => A != k4_tarski(D,E) ) ) ) ) ) ), file(domain_1,t9_domain_1), [interesting(0.00)]). fof(t50_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(k6_borsuk_1(A,B))) => ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & C = k8_borsuk_1(A,B,D,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,t9_domain_1]), [file(borsuk_1,t50_borsuk_1),interesting(0.00)]). fof(t96_funct_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ~ v1_xboole_0(D) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,A,B) & m2_relset_1(E,A,B) ) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,C,D) & m2_relset_1(F,C,D) ) => ! [G] : ( m1_subset_1(G,A) => ! [H] : ( m1_subset_1(H,C) => k1_funct_1(k16_funct_3(A,C,B,D,E,F),k4_tarski(G,H)) = k4_tarski(k8_funct_2(A,B,E,G),k8_funct_2(C,D,F,H)) ) ) ) ) ) ) ) ) ), file(funct_3,t96_funct_3), [interesting(0.00)]). fof(t35_funct_1,theorem,( ! [A,B] : ( r2_hidden(B,A) => k1_funct_1(k6_relat_1(A),B) = B ) ), file(funct_1,t35_funct_1), [interesting(0.00)]). fof(t21_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,A) => ! [F] : ( m1_subset_1(F,C) => k8_funct_2(k2_zfmisc_1(A,C),k2_zfmisc_1(B,C),k16_funct_3(A,C,B,C,D,k6_partfun1(C)),k1_domain_1(A,C,E,F)) = k1_domain_1(B,C,k8_funct_2(A,B,D,E),F) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t96_funct_3,t35_funct_1]), [file(borsuk_1,t21_borsuk_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(t35_zfmisc_1,theorem,( ! [A,B] : k2_zfmisc_1(k1_tarski(A),k1_tarski(B)) = k1_tarski(k4_tarski(A,B)) ), file(zfmisc_1,t35_zfmisc_1), [interesting(0.00)]). fof(t94_funct_3,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => k10_relat_1(k15_funct_3(C,D),k2_zfmisc_1(A,B)) = k2_zfmisc_1(k10_relat_1(C,A),k10_relat_1(D,B)) ) ) ), file(funct_3,t94_funct_3), [interesting(0.00)]). fof(t92_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,A) & v3_funct_2(C,A,A) & m2_relset_1(C,A,A) ) => ( r1_tarski(B,A) => ( k2_funct_2(A,A,C,k3_funct_2(A,A,C,B)) = B & k3_funct_2(A,A,C,k2_funct_2(A,A,C,B)) = B ) ) ) ), file(funct_2,t92_funct_2), [interesting(0.00)]). fof(t162_funct_1,theorem,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => k9_relat_1(k6_relat_1(A),B) = B ) ), file(funct_1,t162_funct_1), [interesting(0.00)]). fof(t24_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,B) => ! [F] : ( m1_subset_1(F,C) => k3_funct_2(k2_zfmisc_1(A,C),k2_zfmisc_1(B,C),k16_funct_3(A,C,B,C,D,k6_partfun1(C)),k6_domain_1(k2_zfmisc_1(B,C),k1_domain_1(B,C,E,F))) = k12_mcart_1(A,C,k3_funct_2(A,B,D,k6_domain_1(B,E)),k6_domain_1(C,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_zfmisc_1,t94_funct_3,t4_borsuk_1]), [file(borsuk_1,t24_borsuk_1),interesting(0.00)]). fof(d15_borsuk_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_borsuk_1(B,A) => ( v2_borsuk_1(B,A) <=> ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(C,B) => v6_compts_1(C,A) ) ) ) ) ) ), file(borsuk_1,d15_borsuk_1), [interesting(0.00)]). fof(t54_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ( v3_pre_topc(C,k6_borsuk_1(A,B)) => C = k5_setfam_1(u1_struct_0(k6_borsuk_1(A,B)),k11_borsuk_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t45_borsuk_1,d3_tarski,d4_tarski,t92_zfmisc_1,d4_tarski,d10_xboole_0,t53_borsuk_1]), [file(borsuk_1,t54_borsuk_1),interesting(0.00)]). fof(t52_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ( r1_tarski(C,D) => r1_tarski(k11_borsuk_1(A,B,C),k11_borsuk_1(A,B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t1_xboole_1]), [file(borsuk_1,t52_borsuk_1),interesting(0.00)]). fof(t95_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => r1_tarski(k3_tarski(A),k3_tarski(B)) ) ), file(zfmisc_1,t95_zfmisc_1), [interesting(0.00)]). fof(d1_tops_2,definition,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ( v1_tops_2(B,A) <=> ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(C,B) => v3_pre_topc(C,A) ) ) ) ) ) ), file(tops_2,d1_tops_2), [interesting(0.00)]). fof(t26_tops_2,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ( v1_tops_2(B,A) => v3_pre_topc(k5_setfam_1(u1_struct_0(A),B),A) ) ) ) ), file(tops_2,t26_tops_2), [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(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(t63_borsuk_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r1_compts_1(A,C,D) & ! [E] : ( m1_subset_1(E,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ~ ( r1_tarski(E,C) & r1_compts_1(A,E,D) & ! [F] : ~ ( r2_hidden(F,E) & r1_xboole_0(F,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_compts_1,s7_domain_1,d3_tarski,d3_tarski,d1_compts_1,d4_tarski,d3_xboole_0,d4_tarski,d7_xboole_0]), [file(borsuk_1,t63_borsuk_1),interesting(0.00)]). fof(t18_tops_2,theorem,( ! [A] : ( l1_pre_topc(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ( ( r1_tarski(B,C) & v1_tops_2(C,A) ) => v1_tops_2(B,A) ) ) ) ) ), file(tops_2,t18_tops_2), [interesting(0.00)]). fof(t8_funct_3,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(k1_funct_3(B))) => k1_funct_1(k1_funct_3(B),A) = k9_relat_1(B,A) ) ) ), file(funct_3,t8_funct_3), [interesting(0.00)]). fof(t149_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => k9_relat_1(A,k1_xboole_0) = k1_xboole_0 ) ), file(relat_1,t149_relat_1), [interesting(0.00)]). fof(t52_tops_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => v3_pre_topc(k1_pre_topc(A),A) ) ), file(tops_1,t52_tops_1), [interesting(0.00)]). fof(t16_funct_3,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(A,k1_zfmisc_1(k1_relat_1(B))) => k9_relat_1(B,k3_tarski(A)) = k3_tarski(k9_relat_1(k1_funct_3(B),A)) ) ) ), file(funct_3,t16_funct_3), [interesting(0.00)]). fof(t16_borsuk_1,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(A))) => k5_setfam_1(B,k2_funct_2(k1_zfmisc_1(A),k1_zfmisc_1(B),k2_funct_3(A,B,C),D)) = k2_funct_2(A,B,C,k5_setfam_1(A,D)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t16_funct_3]), [file(borsuk_1,t16_borsuk_1),interesting(0.00)]). fof(t60_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ( v1_tops_2(C,k6_borsuk_1(A,B)) => ( v1_tops_2(k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(A),k12_borsuk_1(A,B),C),A) & v1_tops_2(k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(B),k13_borsuk_1(A,B),C),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tops_2,t57_borsuk_1,d1_tops_2,t59_borsuk_1,d1_tops_2,t58_borsuk_1,d1_tops_2,t59_borsuk_1]), [file(borsuk_1,t60_borsuk_1),interesting(0.00)]). fof(s1_zfrefle1,theorem, ( ! [A] : ~ ( r2_hidden(A,f1_s1_zfrefle1) & ! [B] : ~ p1_s1_zfrefle1(A,B) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s1_zfrefle1 & ! [B] : ( r2_hidden(B,f1_s1_zfrefle1) => p1_s1_zfrefle1(B,k1_funct_1(A,B)) ) ) ), file(zfrefle1,s1_zfrefle1), [interesting(0.00)]). fof(t17_finset_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( v1_finset_1(A) => v1_finset_1(k9_relat_1(B,A)) ) ) ), file(finset_1,t17_finset_1), [interesting(0.00)]). fof(t64_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ~ ( v1_finset_1(C) & r1_tarski(C,k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(A),k12_borsuk_1(A,B),D)) & ! [E] : ( m1_subset_1(E,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ~ ( r1_tarski(E,D) & v1_finset_1(E) & C = k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(A),k12_borsuk_1(A,B),E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_funct_1,s1_zfrefle1,d3_tarski,d12_funct_1,t1_xboole_1,t17_finset_1,d12_funct_1,d12_funct_1,d12_funct_1]), [file(borsuk_1,t64_borsuk_1),interesting(0.00)]). fof(t2_zfmisc_1,theorem,( k3_tarski(k1_xboole_0) = k1_xboole_0 ), file(zfmisc_1,t2_zfmisc_1), [interesting(0.00)]). fof(t55_tops_1,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( l1_pre_topc(B) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( ( v3_pre_topc(D,B) => k1_tops_1(B,D) = D ) & ( k1_tops_1(A,C) = C => v3_pre_topc(C,A) ) ) ) ) ) ) ), file(tops_1,t55_tops_1), [interesting(0.00)]). fof(t27_tops_2,theorem,( ! [A] : ( ( v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ( ( v1_tops_2(B,A) & v1_finset_1(B) ) => v3_pre_topc(k6_setfam_1(u1_struct_0(A),B),A) ) ) ) ), file(tops_2,t27_tops_2), [interesting(0.00)]). fof(t152_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ~ ( A != k1_xboole_0 & r1_tarski(A,k1_relat_1(B)) & k9_relat_1(B,A) = k1_xboole_0 ) ) ), file(relat_1,t152_relat_1), [interesting(0.00)]). fof(t61_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ( ( k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(A),k12_borsuk_1(A,B),C) = k1_xboole_0 | k14_borsuk_1(u1_struct_0(k6_borsuk_1(A,B)),u1_struct_0(B),k13_borsuk_1(A,B),C) = k1_xboole_0 ) => C = k1_xboole_0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t152_relat_1]), [file(borsuk_1,t61_borsuk_1),interesting(0.00)]). fof(t56_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_pre_topc(B) & l1_pre_topc(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B))))) => ( ! [E] : ( r2_hidden(E,D) => ( r1_tarski(E,C) & ? [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) & ? [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(B))) & E = k7_borsuk_1(A,B,F,G) ) ) ) ) => r1_tarski(k7_borsuk_1(A,B,k5_setfam_1(u1_struct_0(A),k2_funct_2(k1_pcomps_1(u1_struct_0(k6_borsuk_1(A,B))),k1_pcomps_1(u1_struct_0(A)),k12_borsuk_1(A,B),D)),k6_setfam_1(u1_struct_0(B),k2_funct_2(k1_pcomps_1(u1_struct_0(k6_borsuk_1(A,B))),k1_pcomps_1(u1_struct_0(B)),k13_borsuk_1(A,B),D))),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_borsuk_1,t14_borsuk_1]), [file(borsuk_1,t56_borsuk_1),interesting(0.00)]). fof(t2_xboole_1,theorem,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), [interesting(0.00)]). fof(t93_funct_3,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => k9_relat_1(k15_funct_3(C,D),k2_zfmisc_1(A,B)) = k2_zfmisc_1(k9_relat_1(C,A),k9_relat_1(D,B)) ) ) ), file(funct_3,t93_funct_3), [interesting(0.00)]). fof(t23_borsuk_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(C)) => k2_funct_2(k2_zfmisc_1(A,C),k2_zfmisc_1(B,C),k16_funct_3(A,C,B,C,D,k6_partfun1(C)),k12_mcart_1(A,C,E,F)) = k12_mcart_1(B,C,k2_funct_2(A,B,D,E),F) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t93_funct_3,t162_funct_1]), [file(borsuk_1,t23_borsuk_1),interesting(0.00)]). fof(t80_borsuk_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_pre_topc(A) & l1_pre_topc(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_pre_topc(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & m1_eqrel_1(C,u1_struct_0(B)) ) => ! [D] : ( r2_hidden(D,u1_struct_0(B)) => r2_hidden(k1_funct_1(k17_borsuk_1(A,k18_borsuk_1(A,B,C)),D),u1_struct_0(k16_borsuk_1(B,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_borsuk_1,t76_borsuk_1]), [file(borsuk_1,t80_borsuk_1),interesting(0.00)]). fof(t8_borsuk_1,theorem,( $true ), file(borsuk_1,t8_borsuk_1), [interesting(0.00)]).