fof(t24_borsuk_3,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( v2_pre_topc(B)
            & l1_pre_topc(B) )
         => ( ( v2_compts_1(A)
              & v2_compts_1(B) )
           => v2_compts_1(k6_borsuk_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_borsuk_3,t4_borsuk_3,t5_borsuk_3,t4_borsuk_3,t5_borsuk_3,t4_borsuk_3,t5_borsuk_3]),
    [file(borsuk_3,t24_borsuk_3),interesting(1.00)]).

fof(l28_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & v2_compts_1(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(B)
            & l1_pre_topc(B) )
         => v2_compts_1(k6_borsuk_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_compts_1,t23_borsuk_3]),
    [file(borsuk_3,l28_borsuk_3),interesting(0.94)]).

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)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l30_borsuk_3,t17_borsuk_3,t7_tsep_1]),
    [file(borsuk_3,t25_borsuk_3),interesting(0.82)]).

fof(t17_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)
             => m1_pre_topc(k6_borsuk_1(B,C),k6_borsuk_1(B,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_borsuk_1,d5_borsuk_1,t35_borsuk_1,t12_pre_topc,t119_zfmisc_1,d5_pre_topc,t45_borsuk_1,d3_tarski,d3_tarski,d3_tarski,d1_tarski,t31_zfmisc_1,d3_tarski,d1_tarski,d5_pre_topc,d5_borsuk_1,d1_pre_topc,d3_tarski,d4_tarski,t12_pre_topc,d2_zfmisc_1,d5_pre_topc,d9_pre_topc,d3_xboole_0,t106_zfmisc_1,d5_pre_topc,d4_tarski,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,d4_tarski,d2_zfmisc_1,t106_zfmisc_1,t12_pre_topc,d3_xboole_0,t106_zfmisc_1,d4_tarski,d5_pre_topc,t45_borsuk_1,t119_zfmisc_1,t1_jordan1,t12_pre_topc,t12_pre_topc,t44_tops_2,t19_xboole_1,d3_tarski,d3_xboole_0,d4_tarski,d3_xboole_0,t41_tops_2,d4_tarski,d10_xboole_0,d3_tops_2,t1_borsuk_3,t123_zfmisc_1,t17_xboole_1,t12_pre_topc,t38_tops_1,d5_pre_topc,d9_pre_topc,d5_pre_topc,t45_borsuk_1,d5_pre_topc,d9_pre_topc]),
    [file(borsuk_3,t17_borsuk_3),interesting(0.81)]).

fof(l30_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)
             => m1_pre_topc(k6_borsuk_1(C,B),k6_borsuk_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_borsuk_1,d5_borsuk_1,t35_borsuk_1,t12_pre_topc,t119_zfmisc_1,d5_pre_topc,t45_borsuk_1,d3_tarski,d3_tarski,d3_tarski,d1_tarski,t31_zfmisc_1,d3_tarski,d1_tarski,d5_pre_topc,d5_borsuk_1,d1_pre_topc,d3_tarski,d4_tarski,t12_pre_topc,d2_zfmisc_1,d5_pre_topc,d9_pre_topc,d3_xboole_0,t106_zfmisc_1,d5_pre_topc,d4_tarski,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,d4_tarski,d2_zfmisc_1,t106_zfmisc_1,t12_pre_topc,d3_xboole_0,t106_zfmisc_1,d4_tarski,d5_pre_topc,t45_borsuk_1,t119_zfmisc_1,t1_jordan1,t12_pre_topc,t12_pre_topc,t44_tops_2,t19_xboole_1,d3_tarski,d3_xboole_0,d4_tarski,d3_xboole_0,t41_tops_2,d4_tarski,d10_xboole_0,d3_tops_2,t1_borsuk_3,t123_zfmisc_1,t17_xboole_1,t12_pre_topc,t38_tops_1,d5_pre_topc,d9_pre_topc,d5_pre_topc,t45_borsuk_1,d5_pre_topc,d9_pre_topc]),
    [file(borsuk_3,l30_borsuk_3),interesting(0.81)]).

fof(t15_borsuk_3,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))
             => r1_borsuk_3(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_borsuk_1,t1_jordan1,d1_t_0topsp,t11_borsuk_3]),
    [file(borsuk_3,t15_borsuk_3),interesting(0.75)]).

fof(t5_borsuk_3,theorem,(
    ! [A] : 
      ( ( v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => v2_compts_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t9_compts_1,t10_compts_1]),
    [file(borsuk_3,t5_borsuk_3),interesting(0.74)]).

fof(l3_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_pre_topc(A) )
     => r1_t_0topsp(A,A) ) ),
    inference(mizar_proof,[status(thm)],[d1_t_0topsp]),
    [file(borsuk_3,l3_borsuk_3),interesting(0.70)]).

fof(t16_borsuk_3,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) )
         => ( ( r1_borsuk_3(A,B)
              & v2_compts_1(A) )
           => v2_compts_1(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_t_0topsp,d5_tops_2,t23_compts_1]),
    [file(borsuk_3,t16_borsuk_3),interesting(0.70)]).

fof(t4_borsuk_3,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( v3_struct_0(B)
            & v2_pre_topc(B)
            & l1_pre_topc(B) )
         => ( v3_struct_0(k6_borsuk_1(A,B))
            & v3_struct_0(k6_borsuk_1(B,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_borsuk_1,d1_struct_0]),
    [file(borsuk_3,t4_borsuk_3),interesting(0.70)]).

fof(t19_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => v2_compts_1(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C)))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l18_borsuk_3,t16_borsuk_3]),
    [file(borsuk_3,t19_borsuk_3),interesting(0.69)]).

fof(t18_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(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(k6_borsuk_1(B,A))))
                 => ( D = k7_borsuk_1(B,A,k2_pre_topc(B),k1_struct_0(A,C))
                   => v6_compts_1(D,k6_borsuk_1(B,A)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l18_borsuk_3,t16_borsuk_3,l21_borsuk_3,t12_compts_1]),
    [file(borsuk_3,t18_borsuk_3),interesting(0.69)]).

fof(t20_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & v2_compts_1(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
             => ( C = a_2_0_borsuk_3(A,B)
               => ( v1_tops_2(C,A)
                  & r1_compts_1(A,C,k2_pre_topc(A)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tops_2,d3_tarski,t12_pre_topc,t54_borsuk_1,d1_compts_1,t51_borsuk_1,t18_borsuk_3,d7_compts_1,t18_tops_2,d1_compts_1,d3_tarski,t26_tops_2,t14_borsuk_3,d5_pre_topc,d3_tarski,d2_zfmisc_1,t95_zfmisc_1,t1_xboole_1,d1_tarski,t106_zfmisc_1,d4_tarski,d1_compts_1]),
    [file(borsuk_3,t20_borsuk_3),interesting(0.69)]).

fof(l4_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_pre_topc(B) )
         => ( r1_t_0topsp(A,B)
           => r1_t_0topsp(B,A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_t_0topsp,t70_tops_2,d1_t_0topsp]),
    [file(borsuk_3,l4_borsuk_3),interesting(0.67)]).

fof(l18_borsuk_3,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_xboole_0(D)
                    & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) )
                 => ( D = k1_struct_0(A,C)
                   => r1_borsuk_3(k6_borsuk_1(B,k3_pre_topc(A,D)),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_borsuk_3,t44_yellow12,d1_t_0topsp,d1_t_0topsp,t71_tops_2,d1_t_0topsp]),
    [file(borsuk_3,l18_borsuk_3),interesting(0.66)]).

fof(t1_borsuk_3,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( v2_pre_topc(B)
            & l1_pre_topc(B) )
         => k2_pre_topc(k6_borsuk_1(A,B)) = k7_borsuk_1(A,B,k2_pre_topc(A),k2_pre_topc(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_pre_topc,t12_pre_topc,d5_borsuk_1]),
    [file(borsuk_3,t1_borsuk_3),interesting(0.66)]).

fof(t23_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & v2_compts_1(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(B,A)))))
             => ~ ( r1_pre_topc(k6_borsuk_1(B,A),C)
                  & v1_tops_2(C,k6_borsuk_1(B,A))
                  & ! [D] : 
                      ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k6_borsuk_1(B,A)))))
                     => ~ ( r1_tarski(D,C)
                          & r1_pre_topc(k6_borsuk_1(B,A),D)
                          & v1_finset_1(D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t22_borsuk_3,s1_zfrefle1,d3_tarski,d4_tarski,d5_funct_1,t26_finset_1,d5_funct_1,t25_finset_1,d3_tarski,d3_tarski,d4_tarski,d2_zfmisc_1,d4_tarski,t106_zfmisc_1,d3_tarski,d10_xboole_0,d3_tarski,d2_zfmisc_1,d4_tarski,t106_zfmisc_1,d4_tarski,d8_pre_topc,t1_borsuk_3,d3_tarski,d4_tarski,d2_zfmisc_1,d5_funct_1,t106_zfmisc_1,d4_tarski,d4_tarski,d4_tarski,t12_pre_topc,d10_xboole_0,d8_pre_topc]),
    [file(borsuk_3,t23_borsuk_3),interesting(0.66)]).

fof(t21_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & v2_compts_1(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(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(B,A)))))
                 => ( ( r1_pre_topc(k6_borsuk_1(B,A),D)
                      & v1_tops_2(D,k6_borsuk_1(B,A))
                      & C = a_3_2_borsuk_3(A,B,D) )
                   => ( v1_tops_2(C,A)
                      & r1_pre_topc(A,C) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_pre_topc,d1_tops_2,t12_pre_topc,d3_tarski,t12_pre_topc,d1_compts_1,t18_borsuk_3,d7_compts_1,t18_tops_2,d1_compts_1,d3_tarski,t26_tops_2,t14_borsuk_3,d5_pre_topc,d3_tarski,d2_zfmisc_1,d1_tarski,t106_zfmisc_1,d4_tarski,d10_xboole_0,d8_pre_topc]),
    [file(borsuk_3,t21_borsuk_3),interesting(0.65)]).

fof(t3_borsuk_3,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) )
             => ( ( r1_borsuk_3(A,B)
                  & r1_borsuk_3(B,C) )
               => r1_borsuk_3(A,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_t_0topsp,d1_t_0topsp,t71_tops_2,d1_t_0topsp]),
    [file(borsuk_3,t3_borsuk_3),interesting(0.61)]).

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)))) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_xboole_0,d1_xboole_0,d1_struct_0,t26_borsuk_3,t12_compts_1,t9_compts_1,t9_compts_1,t9_compts_1]),
    [file(borsuk_3,t27_borsuk_3),interesting(0.58)]).

fof(t14_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( ( v3_pre_topc(C,k6_borsuk_1(B,A))
                & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(B,A)))) )
             => r2_hidden(a_3_1_borsuk_3(A,B,C),u1_pre_topc(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,s1_xboole_0,d3_tarski,d10_xboole_0,d3_tarski,t13_borsuk_3,d4_tarski,t79_zfmisc_1,t1_xboole_1,d3_tarski,d5_pre_topc,d1_pre_topc]),
    [file(borsuk_3,t14_borsuk_3),interesting(0.55)]).

fof(t22_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & v2_compts_1(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(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(B,A)))))
                 => ~ ( r1_pre_topc(k6_borsuk_1(B,A),D)
                      & v1_tops_2(D,k6_borsuk_1(B,A))
                      & C = a_3_2_borsuk_3(A,B,D)
                      & ! [E] : 
                          ( m1_subset_1(E,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
                         => ~ ( r1_tarski(E,C)
                              & v1_finset_1(E)
                              & r1_pre_topc(A,E) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_borsuk_3,d3_compts_1]),
    [file(borsuk_3,t22_borsuk_3),interesting(0.55)]).

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))) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_borsuk_3,d5_borsuk_1,t1_jordan1,t1_jordan1,t1_jordan1,t4_topmetr,t4_topmetr,t6_tsep_1]),
    [file(borsuk_3,t26_borsuk_3),interesting(0.50)]).

fof(l21_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)))
                 => ( C = k7_borsuk_1(B,A,k2_pre_topc(B),D)
                   => g1_pre_topc(u1_struct_0(k6_borsuk_1(B,k3_pre_topc(A,D))),u1_pre_topc(k6_borsuk_1(B,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))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t17_borsuk_3,d5_borsuk_1,t1_jordan1,t12_pre_topc,t1_jordan1,t4_topmetr,t4_topmetr,t6_tsep_1]),
    [file(borsuk_3,l21_borsuk_3),interesting(0.49)]).

fof(t13_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( ( v3_pre_topc(C,k6_borsuk_1(B,A))
                & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(B,A)))) )
             => ! [D] : ~ ( r2_hidden(D,a_3_1_borsuk_3(A,B,C))
                  & ! [E] : 
                      ( ( v3_pre_topc(E,A)
                        & m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) )
                     => ~ ( r2_hidden(D,E)
                          & r1_tarski(E,a_3_1_borsuk_3(A,B,C)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_compts_1,t55_tops_1,d2_connsp_2,t67_borsuk_1,t44_tops_1,d2_connsp_2,t1_xboole_1,d3_tarski,t37_zfmisc_1,t119_zfmisc_1,t1_xboole_1,d1_connsp_2]),
    [file(borsuk_3,t13_borsuk_3),interesting(0.46)]).

fof(t11_borsuk_3,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(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B)),u1_struct_0(B))
                    & m2_relset_1(D,u1_struct_0(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B)),u1_struct_0(B)) )
                 => ( D = k10_funct_3(k1_struct_0(A,C),u1_struct_0(B))
                   => v3_tops_2(D,k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_jordan1,d1_funct_2,t12_pre_topc,d5_tops_2,t62_funct_3,t12_pre_topc,t7_borsuk_3,t40_yellow12,t2_borsuk_3,t41_yellow12,t9_borsuk_3]),
    [file(borsuk_3,t11_borsuk_3),interesting(0.44)]).

fof(t2_borsuk_3,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))
             => ( v1_funct_1(k3_borsuk_1(B,A,C))
                & v1_funct_2(k3_borsuk_1(B,A,C),u1_struct_0(B),u1_struct_0(k3_pre_topc(A,k1_struct_0(A,C))))
                & v5_pre_topc(k3_borsuk_1(B,A,C),B,k3_pre_topc(A,k1_struct_0(A,C)))
                & m2_relset_1(k3_borsuk_1(B,A,C),u1_struct_0(B),u1_struct_0(k3_pre_topc(A,k1_struct_0(A,C)))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_borsuk_1,d1_tarski,t1_jordan1,t57_funcop_1,t9_topmetr]),
    [file(borsuk_3,t2_borsuk_3),interesting(0.43)]).

fof(t6_borsuk_3,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(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C)))),u1_struct_0(B))
                    & m2_relset_1(D,u1_struct_0(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C)))),u1_struct_0(B)) )
                 => ( D = k9_funct_3(u1_struct_0(B),k1_struct_0(A,C))
                   => v2_funct_1(D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_funct_3,d8_funct_1,d2_zfmisc_1,d2_zfmisc_1,d1_tarski,d1_tarski,d5_funct_3,d5_funct_3]),
    [file(borsuk_3,t6_borsuk_3),interesting(0.37)]).

fof(t7_borsuk_3,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(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B)),u1_struct_0(B))
                    & m2_relset_1(D,u1_struct_0(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B)),u1_struct_0(B)) )
                 => ( D = k10_funct_3(k1_struct_0(A,C),u1_struct_0(B))
                   => v2_funct_1(D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_funct_3,d8_funct_1,d2_zfmisc_1,d2_zfmisc_1,d1_tarski,d1_tarski,d6_funct_3,d6_funct_3]),
    [file(borsuk_3,t7_borsuk_3),interesting(0.37)]).

fof(t10_borsuk_3,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(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C)))),u1_struct_0(B))
                    & m2_relset_1(D,u1_struct_0(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C)))),u1_struct_0(B)) )
                 => ( D = k9_funct_3(u1_struct_0(B),k1_struct_0(A,C))
                   => v3_tops_2(D,k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C))),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_jordan1,d1_funct_2,t12_pre_topc,d5_tops_2,t60_funct_3,t12_pre_topc,t6_borsuk_3,t39_yellow12,t2_borsuk_3,t41_yellow12,t8_borsuk_3]),
    [file(borsuk_3,t10_borsuk_3),interesting(0.31)]).

fof(t8_borsuk_3,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(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C)))),u1_struct_0(B))
                    & m2_relset_1(D,u1_struct_0(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C)))),u1_struct_0(B)) )
                 => ( D = k9_funct_3(u1_struct_0(B),k1_struct_0(A,C))
                   => k2_tops_2(k6_borsuk_1(B,k3_pre_topc(A,k1_struct_0(A,C))),B,D) = k14_funct_3(u1_struct_0(B),u1_struct_0(B),u1_struct_0(A),k7_grcat_1(B),k3_borsuk_1(B,A,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_funct_3,t12_pre_topc,t6_borsuk_3,t2_borsuk_3,t41_yellow12,t71_funct_3,t12_relset_1,t1_jordan1,t12_relset_1,t119_zfmisc_1,t1_xboole_1,d3_tarski,d2_zfmisc_1,d1_tarski,d3_borsuk_1,t13_funcop_1,d1_funct_2,d8_funct_3,t11_grcat_1,d5_funct_1,d10_xboole_0,d5_funct_3,d1_funct_2,d1_funct_2,t12_relset_1,t72_funct_3,d11_grcat_1,t12_pre_topc,t64_funct_1,d4_tops_2]),
    [file(borsuk_3,t8_borsuk_3),interesting(0.26)]).

fof(t9_borsuk_3,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(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B)),u1_struct_0(B))
                    & m2_relset_1(D,u1_struct_0(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B)),u1_struct_0(B)) )
                 => ( D = k10_funct_3(k1_struct_0(A,C),u1_struct_0(B))
                   => k2_tops_2(k6_borsuk_1(k3_pre_topc(A,k1_struct_0(A,C)),B),B,D) = k14_funct_3(u1_struct_0(B),u1_struct_0(A),u1_struct_0(B),k3_borsuk_1(B,A,C),k7_grcat_1(B)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t62_funct_3,t12_pre_topc,t7_borsuk_3,t2_borsuk_3,t41_yellow12,t71_funct_3,t12_relset_1,t1_jordan1,t12_relset_1,t119_zfmisc_1,t1_xboole_1,d3_tarski,d2_zfmisc_1,d1_tarski,d3_borsuk_1,t13_funcop_1,d1_funct_2,d8_funct_3,t11_grcat_1,d5_funct_1,d10_xboole_0,d6_funct_3,d1_funct_2,d1_funct_2,t12_relset_1,t72_funct_3,d11_grcat_1,t12_pre_topc,t64_funct_1,d4_tops_2]),
    [file(borsuk_3,t9_borsuk_3),interesting(0.26)]).

fof(d1_t_0topsp,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( l1_pre_topc(B)
         => ( r1_t_0topsp(A,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) ) ) ) ) ),
    file(t_0topsp,d1_t_0topsp),
    [interesting(0.00)]).

fof(t70_tops_2,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( v3_tops_2(C,A,B)
               => v3_tops_2(k2_tops_2(A,B,C),B,A) ) ) ) ) ),
    file(tops_2,t70_tops_2),
    [interesting(0.00)]).

fof(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(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(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(d5_tops_2,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( l1_pre_topc(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( v3_tops_2(C,A,B)
              <=> ( k1_relat_1(C) = k2_pre_topc(A)
                  & k2_relat_1(C) = k2_pre_topc(B)
                  & v2_funct_1(C)
                  & v5_pre_topc(C,A,B)
                  & v5_pre_topc(k2_tops_2(A,B,C),B,A) ) ) ) ) ) ),
    file(tops_2,d5_tops_2),
    [interesting(0.00)]).

fof(t60_funct_3,theorem,(
    ! [A,B] : 
      ( A != k1_xboole_0
     => k2_relat_1(k7_funct_3(B,A)) = B ) ),
    file(funct_3,t60_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(d8_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(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) )
           => B = C ) ) ) ),
    file(funct_1,d8_funct_1),
    [interesting(0.00)]).

fof(d2_zfmisc_1,definition,(
    ! [A,B,C] : 
      ( C = k2_zfmisc_1(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E,F] : 
              ( r2_hidden(E,A)
              & r2_hidden(F,B)
              & D = k4_tarski(E,F) ) ) ) ),
    file(zfmisc_1,d2_zfmisc_1),
    [interesting(0.00)]).

fof(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [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(d3_borsuk_1,definition,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_struct_0(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k3_borsuk_1(A,B,C) = k1_borsuk_1(u1_struct_0(B),u1_struct_0(A),C) ) ) ) ),
    file(borsuk_1,d3_borsuk_1),
    [interesting(0.00)]).

fof(t57_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(C,B)
     => ( v1_funct_1(k2_funcop_1(A,C))
        & v1_funct_2(k2_funcop_1(A,C),A,B)
        & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ),
    file(funcop_1,t57_funcop_1),
    [interesting(0.00)]).

fof(t9_topmetr,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [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] : 
                  ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
                 => ( v5_pre_topc(C,A,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))) )
                       => ( E = C
                         => v5_pre_topc(E,A,k3_pre_topc(B,D)) ) ) ) ) ) ) ) ),
    file(topmetr,t9_topmetr),
    [interesting(0.00)]).

fof(t41_yellow12,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v2_pre_topc(C)
                & l1_pre_topc(C) )
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
                    & v5_pre_topc(D,A,B)
                    & m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) )
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,u1_struct_0(A),u1_struct_0(C))
                        & v5_pre_topc(E,A,C)
                        & m2_relset_1(E,u1_struct_0(A),u1_struct_0(C)) )
                     => ( v1_funct_1(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E))
                        & v1_funct_2(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),u1_struct_0(A),u1_struct_0(k6_borsuk_1(B,C)))
                        & v5_pre_topc(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),A,k6_borsuk_1(B,C))
                        & m2_relset_1(k14_funct_3(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),u1_struct_0(A),u1_struct_0(k6_borsuk_1(B,C))) ) ) ) ) ) ) ),
    file(yellow12,t41_yellow12),
    [interesting(0.00)]).

fof(t71_funct_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => r1_tarski(k2_relat_1(k13_funct_3(A,B)),k2_zfmisc_1(k2_relat_1(A),k2_relat_1(B))) ) ) ),
    file(funct_3,t71_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(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(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(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(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(d8_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 = k13_funct_3(A,B)
              <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B))
                  & ! [D] : 
                      ( r2_hidden(D,k1_relat_1(C))
                     => k1_funct_1(C,D) = k4_tarski(k1_funct_1(A,D),k1_funct_1(B,D)) ) ) ) ) ) ) ),
    file(funct_3,d8_funct_3),
    [interesting(0.00)]).

fof(t11_grcat_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_struct_0(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k8_funct_2(u1_struct_0(A),u1_struct_0(A),k7_grcat_1(A),B) = B ) ) ),
    file(grcat_1,t11_grcat_1),
    [interesting(0.00)]).

fof(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(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(t72_funct_3,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ! [D] : 
          ( ( v1_relat_1(D)
            & v1_funct_1(D) )
         => ( ( k1_relat_1(C) = k1_relat_1(D)
              & r1_tarski(k2_relat_1(C),A)
              & r1_tarski(k2_relat_1(D),B) )
           => ( k5_relat_1(k13_funct_3(C,D),k9_funct_3(A,B)) = C
              & k5_relat_1(k13_funct_3(C,D),k10_funct_3(A,B)) = D ) ) ) ) ),
    file(funct_3,t72_funct_3),
    [interesting(0.00)]).

fof(d11_grcat_1,definition,(
    ! [A] : 
      ( l1_struct_0(A)
     => k7_grcat_1(A) = k6_partfun1(u1_struct_0(A)) ) ),
    file(grcat_1,d11_grcat_1),
    [interesting(0.00)]).

fof(t64_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( v2_funct_1(A)
              & k2_relat_1(B) = k1_relat_1(A)
              & k5_relat_1(B,A) = k6_relat_1(k2_relat_1(A)) )
           => B = k2_funct_1(A) ) ) ) ),
    file(funct_1,t64_funct_1),
    [interesting(0.00)]).

fof(d4_tops_2,definition,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( l1_struct_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( ( k2_relat_1(C) = k2_pre_topc(B)
                  & v2_funct_1(C) )
               => k2_tops_2(A,B,C) = k2_funct_1(C) ) ) ) ) ),
    file(tops_2,d4_tops_2),
    [interesting(0.00)]).

fof(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)) ) ) ) ) ),
    file(borsuk_1,t54_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(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(d6_borsuk_1,definition,(
    ! [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))))
             => k11_borsuk_1(A,B,C) = a_3_1_borsuk_1(A,B,C) ) ) ) ),
    file(borsuk_1,d6_borsuk_1),
    [interesting(0.00)]).

fof(s3_pboole,theorem,
    ( ! [A] : ~ ( r2_hidden(A,f1_s3_pboole)
        & ! [B] : ~ p1_s3_pboole(A,B) )
   => ? [A] : 
        ( m1_pboole(A,f1_s3_pboole)
        & ! [B] : 
            ( r2_hidden(B,f1_s3_pboole)
           => p1_s3_pboole(B,k1_funct_1(A,B)) ) ) ),
    file(pboole,s3_pboole),
    [interesting(0.00)]).

fof(t12_borsuk_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v2_pre_topc(B)
            & v2_compts_1(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( ( v3_pre_topc(C,k6_borsuk_1(A,B))
                & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k6_borsuk_1(A,B)))) )
             => ! [D] : ~ ( r2_hidden(D,a_3_0_borsuk_3(A,B,C))
                  & ! [E] : 
                      ( m1_pboole(E,u1_struct_0(B))
                     => ? [F] : 
                          ( r2_hidden(F,u1_struct_0(B))
                          & ! [G] : 
                              ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A)))
                             => ! [H] : 
                                  ( m1_subset_1(H,k1_zfmisc_1(u1_struct_0(B)))
                                 => ~ ( k1_funct_1(E,F) = k4_tarski(G,H)
                                      & r2_hidden(k4_tarski(D,F),k7_borsuk_1(A,B,G,H))
                                      & v3_pre_topc(G,A)
                                      & v3_pre_topc(H,B)
                                      & r1_tarski(k7_borsuk_1(A,B,G,H),C) ) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t54_borsuk_1,d1_tarski,t106_zfmisc_1,d4_tarski,d6_borsuk_1,s3_pboole]),
    [file(borsuk_3,t12_borsuk_3),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(t62_funct_3,theorem,(
    ! [A,B] : 
      ( A != k1_xboole_0
     => k2_relat_1(k8_funct_3(A,B)) = B ) ),
    file(funct_3,t62_funct_3),
    [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(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(t44_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) )
         => r1_t_0topsp(k6_borsuk_1(A,B),k6_borsuk_1(B,A)) ) ) ),
    file(yellow12,t44_yellow12),
    [interesting(0.00)]).

fof(t71_tops_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(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(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(B),u1_struct_0(C))
                        & m2_relset_1(E,u1_struct_0(B),u1_struct_0(C)) )
                     => ( ( v3_tops_2(D,A,B)
                          & v3_tops_2(E,B,C) )
                       => v3_tops_2(k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),A,C) ) ) ) ) ) ) ),
    file(tops_2,t71_tops_2),
    [interesting(0.00)]).

fof(t23_compts_1,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)) )
             => ( ( v2_compts_1(A)
                  & v5_pre_topc(C,A,B)
                  & k2_relat_1(C) = k2_pre_topc(B) )
               => v2_compts_1(B) ) ) ) ) ),
    file(compts_1,t23_compts_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(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(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)) ) ) ) ),
    file(borsuk_1,t51_borsuk_1),
    [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(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) ) ) ) ) ) ) ) ) ) ),
    file(borsuk_1,t45_borsuk_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(d1_pre_topc,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ( v2_pre_topc(A)
      <=> ( r2_hidden(u1_struct_0(A),u1_pre_topc(A))
          & ! [B] : 
              ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
             => ( r1_tarski(B,u1_pre_topc(A))
               => r2_hidden(k5_setfam_1(u1_struct_0(A),B),u1_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)))
                 => ( ( r2_hidden(B,u1_pre_topc(A))
                      & r2_hidden(C,u1_pre_topc(A)) )
                   => r2_hidden(k5_subset_1(u1_struct_0(A),B,C),u1_pre_topc(A)) ) ) ) ) ) ) ),
    file(pre_topc,d1_pre_topc),
    [interesting(0.00)]).

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(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(t44_tops_2,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(k1_zfmisc_1(u1_struct_0(A))))
             => r1_tarski(k5_setfam_1(u1_struct_0(k3_pre_topc(A,B)),k1_tops_2(A,B,C)),k5_setfam_1(u1_struct_0(A),C)) ) ) ) ),
    file(tops_2,t44_tops_2),
    [interesting(0.00)]).

fof(t19_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(A,C) )
     => r1_tarski(A,k3_xboole_0(B,C)) ) ),
    file(xboole_1,t19_xboole_1),
    [interesting(0.00)]).

fof(t41_tops_2,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)))
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
                 => ( r2_hidden(B,D)
                   => r2_hidden(k5_subset_1(u1_struct_0(A),B,C),k1_tops_2(A,C,D)) ) ) ) ) ) ),
    file(tops_2,t41_tops_2),
    [interesting(0.00)]).

fof(d3_tops_2,definition,(
    ! [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(k1_zfmisc_1(u1_struct_0(A))))
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(k3_pre_topc(A,B)))))
                 => ( D = k1_tops_2(A,B,C)
                  <=> ! [E] : 
                        ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(k3_pre_topc(A,B))))
                       => ( r2_hidden(E,D)
                        <=> ? [F] : 
                              ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A)))
                              & r2_hidden(F,C)
                              & k5_subset_1(u1_struct_0(A),F,B) = E ) ) ) ) ) ) ) ) ),
    file(tops_2,d3_tops_2),
    [interesting(0.00)]).

fof(t123_zfmisc_1,theorem,(
    ! [A,B,C,D] : k2_zfmisc_1(k3_xboole_0(A,B),k3_xboole_0(C,D)) = k3_xboole_0(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ),
    file(zfmisc_1,t123_zfmisc_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(t38_tops_1,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
             => ( ( v3_pre_topc(B,A)
                  & v3_pre_topc(C,A) )
               => v3_pre_topc(k5_subset_1(u1_struct_0(A),B,C),A) ) ) ) ) ),
    file(tops_1,t38_tops_1),
    [interesting(0.00)]).

fof(t4_topmetr,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( m1_pre_topc(B,A)
         => ! [C] : 
              ( m1_pre_topc(C,A)
             => ( r1_tarski(u1_struct_0(B),u1_struct_0(C))
               => m1_pre_topc(B,C) ) ) ) ) ),
    file(topmetr,t4_topmetr),
    [interesting(0.00)]).

fof(t6_tsep_1,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( m1_pre_topc(B,A)
         => ! [C] : 
              ( m1_pre_topc(C,A)
             => ( ( m1_pre_topc(B,C)
                  & m1_pre_topc(C,B) )
               => g1_pre_topc(u1_struct_0(B),u1_pre_topc(B)) = g1_pre_topc(u1_struct_0(C),u1_pre_topc(C)) ) ) ) ) ),
    file(tsep_1,t6_tsep_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(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(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(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(s1_xboole_0,theorem,(
    ? [A] : 
    ! [B] : 
      ( r2_hidden(B,A)
    <=> ( r2_hidden(B,f1_s1_xboole_0)
        & p1_s1_xboole_0(B) ) ) ),
    file(xboole_0,s1_xboole_0),
    [interesting(0.00)]).

fof(t10_compts_1,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ( v2_compts_1(A)
      <=> v6_compts_1(k2_pre_topc(A),A) ) ) ),
    file(compts_1,t10_compts_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(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(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) ) ) ) ) ) ) ) ) ),
    file(borsuk_1,t67_borsuk_1),
    [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(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(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(t79_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => r1_tarski(k1_zfmisc_1(A),k1_zfmisc_1(B)) ) ),
    file(zfmisc_1,t79_zfmisc_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(d3_compts_1,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ( v2_compts_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
           => ~ ( r1_pre_topc(A,B)
                & v1_tops_2(B,A)
                & ! [C] : 
                    ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
                   => ~ ( r1_tarski(C,B)
                        & r1_pre_topc(A,C)
                        & v1_finset_1(C) ) ) ) ) ) ) ),
    file(compts_1,d3_compts_1),
    [interesting(0.00)]).

fof(d8_pre_topc,definition,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
         => ( r1_pre_topc(A,B)
          <=> k2_pre_topc(A) = k5_setfam_1(u1_struct_0(A),B) ) ) ) ),
    file(pre_topc,d8_pre_topc),
    [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(t26_finset_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v1_finset_1(k1_relat_1(A))
       => v1_finset_1(k2_relat_1(A)) ) ) ),
    file(finset_1,t26_finset_1),
    [interesting(0.00)]).

fof(t25_finset_1,theorem,(
    ! [A] : 
      ( ( v1_finset_1(A)
        & ! [B] : 
            ( r2_hidden(B,A)
           => v1_finset_1(B) ) )
    <=> v1_finset_1(k3_tarski(A)) ) ),
    file(finset_1,t25_finset_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(t9_compts_1,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => v6_compts_1(k1_pre_topc(A),A) ) ),
    file(compts_1,t9_compts_1),
    [interesting(0.00)]).

fof(d1_xboole_0,definition,(
    ! [A] : 
      ( A = k1_xboole_0
    <=> ! [B] : ~ r2_hidden(B,A) ) ),
    file(xboole_0,d1_xboole_0),
    [interesting(0.00)]).

fof(t7_tsep_1,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( m1_pre_topc(B,A)
         => ! [C] : 
              ( m1_pre_topc(C,B)
             => m1_pre_topc(C,A) ) ) ) ),
    file(tsep_1,t7_tsep_1),
    [interesting(0.00)]).