fof(t2_cantor_1,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => m1_cantor_1(u1_pre_topc(A),A) ) ),
    inference(mizar_proof,[status(thm)],[t1_cantor_1,d2_cantor_1]),
    [file(cantor_1,t2_cantor_1),interesting(1.00)]).

fof(t13_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => k2_cantor_1(A,B) = k2_cantor_1(A,k2_cantor_1(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[t4_cantor_1,d10_xboole_0,d3_tarski,d4_cantor_1,d4_cantor_1,s1_funct_2,d1_funct_2,t26_finset_1,d5_funct_1,d1_funct_2,d1_funct_2,t25_finset_1,t12_relset_1,t95_zfmisc_1,t99_zfmisc_1,t1_xboole_1,d3_tarski,d1_funct_2,d5_funct_1,d3_tarski,d5_funct_1,d1_funct_2,d1_funct_2,d10_xboole_0,t12_relset_1,t79_zfmisc_1,t1_xboole_1,d3_tarski,d10_xboole_0,d3_tarski,t12_cantor_1,d1_funct_2,t60_relat_1,t64_relat_1,t2_zfmisc_1,d4_cantor_1]),
    [file(cantor_1,t13_cantor_1),interesting(0.91)]).

fof(t4_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => r1_tarski(B,k2_cantor_1(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t63_subset_1,t11_setfam_1,t37_zfmisc_1,d10_setfam_1,d4_cantor_1]),
    [file(cantor_1,t4_cantor_1),interesting(0.85)]).

fof(t3_cantor_1,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => v1_tops_2(u1_pre_topc(A),A) ) ),
    inference(mizar_proof,[status(thm)],[d1_tops_2,d5_pre_topc]),
    [file(cantor_1,t3_cantor_1),interesting(0.85)]).

fof(t1_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => r1_tarski(B,k1_cantor_1(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t63_subset_1,t31_zfmisc_1,t37_zfmisc_1,d1_cantor_1]),
    [file(cantor_1,t1_cantor_1),interesting(0.83)]).

fof(t8_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => r2_hidden(A,k2_cantor_1(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[t2_xboole_1,d10_setfam_1,t2_xboole_1,d4_cantor_1]),
    [file(cantor_1,t8_cantor_1),interesting(0.82)]).

fof(t15_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C,D] : 
          ( ( r1_tarski(C,k2_cantor_1(A,B))
            & r1_tarski(D,k2_cantor_1(A,B)) )
         => r1_tarski(k3_setfam_1(C,D),k2_cantor_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d5_setfam_1,t38_zfmisc_1,t12_setfam_1,d10_setfam_1,t38_zfmisc_1,d4_cantor_1,t13_cantor_1]),
    [file(cantor_1,t15_cantor_1),interesting(0.61)]).

fof(t6_cantor_1,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => u1_pre_topc(A) = k1_cantor_1(u1_struct_0(A),u1_pre_topc(A)) ) ),
    inference(mizar_proof,[status(thm)],[t1_cantor_1,d10_xboole_0,d3_tarski,d1_cantor_1,d1_pre_topc]),
    [file(cantor_1,t6_cantor_1),interesting(0.56)]).

fof(t9_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( r1_tarski(B,C)
           => r1_tarski(k1_cantor_1(A,B),k1_cantor_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d1_cantor_1,t1_xboole_1,d1_cantor_1]),
    [file(cantor_1,t9_cantor_1),interesting(0.53)]).

fof(t16_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( r1_tarski(B,C)
           => r1_tarski(k2_cantor_1(A,B),k2_cantor_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d4_cantor_1,t1_xboole_1,d4_cantor_1]),
    [file(cantor_1,t16_cantor_1),interesting(0.52)]).

fof(t18_cantor_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => m1_cantor_1(B,g1_pre_topc(A,k1_cantor_1(A,B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_cantor_1,d2_cantor_1]),
    [file(cantor_1,t18_cantor_1),interesting(0.51)]).

fof(t17_cantor_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => v2_pre_topc(g1_pre_topc(A,k1_cantor_1(A,k2_cantor_1(A,B)))) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_cantor_1,t80_zfmisc_1,t37_zfmisc_1,t31_zfmisc_1,d1_cantor_1,d1_pre_topc,s3_subset_1,t17_borsuk_1,d1_cantor_1,d3_tarski,d10_xboole_0,d3_tarski,t1_xboole_1,d1_cantor_1,d1_cantor_1,d1_cantor_1,t15_cantor_1,t1_xboole_1,t39_setfam_1,d1_cantor_1]),
    [file(cantor_1,t17_cantor_1),interesting(0.49)]).

fof(t5_cantor_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => u1_pre_topc(A) = k2_cantor_1(u1_struct_0(A),u1_pre_topc(A)) ) ),
    inference(mizar_proof,[status(thm)],[t4_cantor_1,d10_xboole_0,t5_pre_topc,t2_setfam_1,t11_setfam_1,t10_setfam_1,d1_pre_topc,s4_setwiseo,d4_cantor_1,d10_setfam_1,d5_finsub_1,d10_setfam_1,d1_pre_topc,t7_subset_1]),
    [file(cantor_1,t5_cantor_1),interesting(0.39)]).

fof(t14_cantor_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C,D] : 
          ( ( r2_hidden(C,k2_cantor_1(A,B))
            & r2_hidden(D,k2_cantor_1(A,B)) )
         => r2_hidden(k3_xboole_0(C,D),k2_cantor_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t38_zfmisc_1,t12_setfam_1,d10_setfam_1,t38_zfmisc_1,d4_cantor_1,t13_cantor_1]),
    [file(cantor_1,t14_cantor_1),interesting(0.38)]).

fof(t20_cantor_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
         => m2_cantor_1(B,g1_pre_topc(A,k1_cantor_1(A,k2_cantor_1(A,B)))) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_cantor_1,t4_cantor_1,t1_xboole_1,d5_cantor_1,t18_cantor_1]),
    [file(cantor_1,t20_cantor_1),interesting(0.23)]).

fof(t7_cantor_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => u1_pre_topc(A) = k1_cantor_1(u1_struct_0(A),k2_cantor_1(u1_struct_0(A),u1_pre_topc(A))) ) ),
    inference(mizar_proof,[status(thm)],[t5_cantor_1,t6_cantor_1]),
    [file(cantor_1,t7_cantor_1),interesting(0.18)]).

fof(t19_cantor_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_pre_topc(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v1_pre_topc(B)
            & v2_pre_topc(B)
            & l1_pre_topc(B) )
         => ! [C] : 
              ( m2_cantor_1(C,A)
             => ( ( u1_struct_0(A) = u1_struct_0(B)
                  & m2_cantor_1(C,B) )
               => A = B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_cantor_1,d2_cantor_1,t9_cantor_1,t1_xboole_1,d5_cantor_1,d2_cantor_1,t7_cantor_1,t7_cantor_1,t9_cantor_1,t1_xboole_1,d5_cantor_1,t16_cantor_1,t9_cantor_1,d10_xboole_0,d5_cantor_1,t16_cantor_1,t9_cantor_1,d10_xboole_0]),
    [file(cantor_1,t19_cantor_1),interesting(0.17)]).

fof(t10_cantor_1,theorem,(
    $true ),
    file(cantor_1,t10_cantor_1),
    [interesting(0.00)]).

fof(t11_cantor_1,theorem,(
    $true ),
    file(cantor_1,t11_cantor_1),
    [interesting(0.00)]).

fof(t38_zfmisc_1,theorem,(
    ! [A,B,C] : 
      ( r1_tarski(k2_tarski(A,B),C)
    <=> ( r2_hidden(A,C)
        & r2_hidden(B,C) ) ) ),
    file(zfmisc_1,t38_zfmisc_1),
    [interesting(0.00)]).

fof(t12_setfam_1,theorem,(
    ! [A,B] : k1_setfam_1(k2_tarski(A,B)) = k3_xboole_0(A,B) ),
    file(setfam_1,t12_setfam_1),
    [interesting(0.00)]).

fof(d10_setfam_1,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( ( B != k1_xboole_0
         => k8_setfam_1(A,B) = k6_setfam_1(A,B) )
        & ( B = k1_xboole_0
         => k8_setfam_1(A,B) = A ) ) ) ),
    file(setfam_1,d10_setfam_1),
    [interesting(0.00)]).

fof(d4_cantor_1,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( C = k2_cantor_1(A,B)
          <=> ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ( r2_hidden(D,C)
                <=> ? [E] : 
                      ( m1_subset_1(E,k1_zfmisc_1(k1_zfmisc_1(A)))
                      & r1_tarski(E,B)
                      & v1_finset_1(E)
                      & D = k8_setfam_1(A,E) ) ) ) ) ) ) ),
    file(cantor_1,d4_cantor_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(t63_subset_1,theorem,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => m1_subset_1(k1_tarski(A),k1_zfmisc_1(B)) ) ),
    file(subset_1,t63_subset_1),
    [interesting(0.00)]).

fof(t11_setfam_1,theorem,(
    ! [A] : k1_setfam_1(k1_tarski(A)) = A ),
    file(setfam_1,t11_setfam_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(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(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(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(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(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(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(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(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(t99_zfmisc_1,theorem,(
    ! [A] : k3_tarski(k1_zfmisc_1(A)) = A ),
    file(zfmisc_1,t99_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(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(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(t58_setfam_1,theorem,(
    ! [A,B,C] : 
      ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( r2_hidden(B,A)
       => ( r2_hidden(B,k8_setfam_1(A,C))
        <=> ! [D] : 
              ( r2_hidden(D,C)
             => r2_hidden(B,D) ) ) ) ) ),
    file(setfam_1,t58_setfam_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(t59_setfam_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( r1_tarski(B,C)
           => r1_tarski(k8_setfam_1(A,C),k8_setfam_1(A,B)) ) ) ) ),
    file(setfam_1,t59_setfam_1),
    [interesting(0.00)]).

fof(t12_cantor_1,theorem,(
    ! [A,B] : 
      ( ( ~ v1_xboole_0(B)
        & m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(A)))) )
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( C = a_2_0_cantor_1(A,B)
           => k8_setfam_1(A,C) = k8_setfam_1(A,k5_setfam_1(k1_zfmisc_1(A),B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_tarski,t58_setfam_1,t58_setfam_1,t58_setfam_1,d3_tarski,d10_xboole_0,d3_tarski,t92_zfmisc_1,t59_setfam_1,t58_setfam_1]),
    [file(cantor_1,t12_cantor_1),interesting(0.00)]).

fof(t60_relat_1,theorem,
    ( k1_relat_1(k1_xboole_0) = k1_xboole_0
    & k2_relat_1(k1_xboole_0) = k1_xboole_0 ),
    file(relat_1,t60_relat_1),
    [interesting(0.00)]).

fof(t64_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( ( k1_relat_1(A) = k1_xboole_0
          | k2_relat_1(A) = k1_xboole_0 )
       => A = k1_xboole_0 ) ) ),
    file(relat_1,t64_relat_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(t2_xboole_1,theorem,(
    ! [A] : r1_tarski(k1_xboole_0,A) ),
    file(xboole_1,t2_xboole_1),
    [interesting(0.00)]).

fof(t80_zfmisc_1,theorem,(
    ! [A] : r1_tarski(k1_tarski(A),k1_zfmisc_1(A)) ),
    file(zfmisc_1,t80_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(d1_cantor_1,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
         => ( C = k1_cantor_1(A,B)
          <=> ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ( r2_hidden(D,C)
                <=> ? [E] : 
                      ( m1_subset_1(E,k1_zfmisc_1(k1_zfmisc_1(A)))
                      & r1_tarski(E,B)
                      & D = k5_setfam_1(A,E) ) ) ) ) ) ) ),
    file(cantor_1,d1_cantor_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(s3_subset_1,theorem,(
    ? [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(f1_s3_subset_1))
      & ! [B] : 
          ( m1_subset_1(B,f1_s3_subset_1)
         => ( r2_hidden(B,A)
          <=> p1_s3_subset_1(B) ) ) ) ),
    file(subset_1,s3_subset_1),
    [interesting(0.00)]).

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)) ) ),
    file(borsuk_1,t17_borsuk_1),
    [interesting(0.00)]).

fof(d5_setfam_1,definition,(
    ! [A,B,C] : 
      ( C = k3_setfam_1(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E,F] : 
              ( r2_hidden(E,A)
              & r2_hidden(F,B)
              & D = k3_xboole_0(E,F) ) ) ) ),
    file(setfam_1,d5_setfam_1),
    [interesting(0.00)]).

fof(t39_setfam_1,theorem,(
    ! [A,B] : k3_tarski(k3_setfam_1(A,B)) = k3_xboole_0(k3_tarski(A),k3_tarski(B)) ),
    file(setfam_1,t39_setfam_1),
    [interesting(0.00)]).

fof(d5_cantor_1,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
         => ( m2_cantor_1(B,A)
          <=> ( r1_tarski(B,u1_pre_topc(A))
              & ? [C] : 
                  ( m1_cantor_1(C,A)
                  & r1_tarski(C,k2_cantor_1(u1_struct_0(A),B)) ) ) ) ) ) ),
    file(cantor_1,d5_cantor_1),
    [interesting(0.00)]).

fof(d2_cantor_1,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
         => ( m1_cantor_1(B,A)
          <=> ( r1_tarski(B,u1_pre_topc(A))
              & r1_tarski(u1_pre_topc(A),k1_cantor_1(u1_struct_0(A),B)) ) ) ) ) ),
    file(cantor_1,d2_cantor_1),
    [interesting(0.00)]).

fof(t5_pre_topc,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => r2_hidden(k1_xboole_0,u1_pre_topc(A)) ) ),
    file(pre_topc,t5_pre_topc),
    [interesting(0.00)]).

fof(t2_setfam_1,theorem,(
    k1_setfam_1(k1_xboole_0) = k1_xboole_0 ),
    file(setfam_1,t2_setfam_1),
    [interesting(0.00)]).

fof(t10_setfam_1,theorem,(
    ! [A,B] : ~ ( A != k1_xboole_0
      & B != k1_xboole_0
      & k1_setfam_1(k2_xboole_0(A,B)) != k3_xboole_0(k1_setfam_1(A),k1_setfam_1(B)) ) ),
    file(setfam_1,t10_setfam_1),
    [interesting(0.00)]).

fof(s4_setwiseo,theorem,
    ( ( p1_s4_setwiseo(k1_setwiseo(f1_s4_setwiseo))
      & ! [A] : 
          ( m1_subset_1(A,k5_finsub_1(f1_s4_setwiseo))
         => ! [B] : 
              ( m1_subset_1(B,f1_s4_setwiseo)
             => ( p1_s4_setwiseo(A)
               => p1_s4_setwiseo(k5_setwiseo(f1_s4_setwiseo,A,k2_setwiseo(f1_s4_setwiseo,B))) ) ) ) )
   => ! [A] : 
        ( m1_subset_1(A,k5_finsub_1(f1_s4_setwiseo))
       => p1_s4_setwiseo(A) ) ),
    file(setwiseo,s4_setwiseo),
    [interesting(0.00)]).

fof(d5_finsub_1,definition,(
    ! [A,B] : 
      ( v4_finsub_1(B)
     => ( B = k5_finsub_1(A)
      <=> ! [C] : 
            ( r2_hidden(C,B)
          <=> ( r1_tarski(C,A)
              & v1_finset_1(C) ) ) ) ) ),
    file(finsub_1,d5_finsub_1),
    [interesting(0.00)]).

fof(t7_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( ! [D] : 
                ( m1_subset_1(D,A)
               => ( r2_hidden(D,B)
                 => r2_hidden(D,C) ) )
           => r1_tarski(B,C) ) ) ) ),
    file(subset_1,t7_subset_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(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)]).