fof(t42_pre_topc,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => v4_pre_topc(k2_pre_topc(A),A) ) ),
    inference(mizar_proof,[status(thm)],[t23_pre_topc,t5_pre_topc,d5_pre_topc,d6_pre_topc]),
    [file(pre_topc,t42_pre_topc),interesting(1.00)]).

fof(t48_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => r1_tarski(B,k6_pre_topc(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_pre_topc,d3_tarski]),
    [file(pre_topc,t48_pre_topc),interesting(0.94)]).

fof(t5_pre_topc,theorem,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => r2_hidden(k1_xboole_0,u1_pre_topc(A)) ) ),
    inference(mizar_proof,[status(thm)],[t2_xboole_1,t2_xboole_1,t2_zfmisc_1,d1_pre_topc]),
    [file(pre_topc,t5_pre_topc),interesting(0.92)]).

fof(t52_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ( ( v4_pre_topc(B,A)
             => k6_pre_topc(A,B) = B )
            & ( ( v2_pre_topc(A)
                & k6_pre_topc(A,B) = B )
             => v4_pre_topc(B,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_pre_topc,t45_pre_topc,d3_tarski,d10_xboole_0,t46_pre_topc,t44_pre_topc]),
    [file(pre_topc,t52_pre_topc),interesting(0.82)]).

fof(l37_pre_topc,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(pre_topc,l37_pre_topc),interesting(0.77)]).

fof(t39_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_pre_topc(B,A)
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
             => m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_pre_topc,t1_xboole_1]),
    [file(pre_topc,t39_pre_topc),interesting(0.74)]).

fof(t49_pre_topc,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)))
             => ( r1_tarski(B,C)
               => r1_tarski(k6_pre_topc(A,B),k6_pre_topc(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_xboole_1,t45_pre_topc,t45_pre_topc,d3_tarski]),
    [file(pre_topc,t49_pre_topc),interesting(0.74)]).

fof(t27_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => k2_pre_topc(A) = k3_subset_1(u1_struct_0(A),k1_pre_topc(A)) ) ),
    inference(mizar_proof,[status(thm)],[d4_subset_1,t22_subset_1]),
    [file(pre_topc,t27_pre_topc),interesting(0.58)]).

fof(t47_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_pre_topc(B,A)
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B)))
                 => ( C = D
                   => k6_pre_topc(B,D) = k3_xboole_0(k6_pre_topc(A,C),k2_pre_topc(B)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_xboole_1,t17_xboole_1,t43_pre_topc,t45_pre_topc,d3_xboole_0,t39_pre_topc,t45_pre_topc,d3_xboole_0,d3_xboole_0,t43_pre_topc,t17_xboole_1,t1_xboole_1,t45_pre_topc,d3_xboole_0,t45_pre_topc,t2_tarski]),
    [file(pre_topc,t47_pre_topc),interesting(0.58)]).

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 ) ) ),
    inference(mizar_proof,[status(thm)],[t28_xboole_1]),
    [file(pre_topc,t15_pre_topc),interesting(0.55)]).

fof(t22_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => k6_subset_1(u1_struct_0(A),k2_pre_topc(A),k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B)) = B ) ) ),
    inference(mizar_proof,[status(thm)],[t48_xboole_1,t15_pre_topc]),
    [file(pre_topc,t22_pre_topc),interesting(0.53)]).

fof(t44_pre_topc,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))))
         => ( ! [C] : 
                ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
               => ( r2_hidden(C,B)
                 => v4_pre_topc(C,A) ) )
           => v4_pre_topc(k6_setfam_1(u1_struct_0(A),B),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s3_subset_1,t22_pre_topc,d6_pre_topc,d5_pre_topc,d3_tarski,d1_pre_topc,d5_pre_topc,t22_pre_topc,d6_pre_topc,d4_xboole_0,t22_pre_topc,d4_xboole_0,d4_xboole_0,d4_tarski,d1_setfam_1,d1_setfam_1,d4_tarski,d4_xboole_0,t2_tarski,d1_pre_topc,d5_pre_topc,d6_pre_topc,d1_setfam_1]),
    [file(pre_topc,t44_pre_topc),interesting(0.52)]).

fof(t43_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_pre_topc(B,A)
         => ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))
             => ( v4_pre_topc(C,B)
              <=> ? [D] : 
                    ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
                    & v4_pre_topc(D,A)
                    & k3_xboole_0(D,k2_pre_topc(B)) = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t39_pre_topc,d6_pre_topc,d5_pre_topc,d9_pre_topc,d5_pre_topc,t22_pre_topc,d6_pre_topc,t17_pre_topc,t32_subset_1,t47_xboole_1,t22_pre_topc,d6_pre_topc,d5_pre_topc,t47_xboole_1,t32_subset_1,t17_pre_topc,t17_xboole_1,d9_pre_topc,d5_pre_topc,d6_pre_topc]),
    [file(pre_topc,t43_pre_topc),interesting(0.48)]).

fof(t45_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ! [C] : 
              ( r2_hidden(C,u1_struct_0(A))
             => ( r2_hidden(C,k6_pre_topc(A,B))
              <=> ! [D] : 
                    ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
                   => ( ( v4_pre_topc(D,A)
                        & r1_tarski(B,D) )
                     => r2_hidden(C,D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_pre_topc,d13_pre_topc,t43_subset_1,d4_xboole_0,t17_pre_topc,t22_pre_topc,t22_pre_topc,d6_pre_topc,t17_pre_topc,t43_subset_1,d4_xboole_0,d13_pre_topc]),
    [file(pre_topc,t45_pre_topc),interesting(0.48)]).

fof(t17_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => k3_subset_1(u1_struct_0(A),B) = k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_subset_1]),
    [file(pre_topc,t17_pre_topc),interesting(0.42)]).

fof(t50_pre_topc,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)))
             => k6_pre_topc(A,k4_subset_1(u1_struct_0(A),B,C)) = k4_subset_1(u1_struct_0(A),k6_pre_topc(A,B),k6_pre_topc(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_xboole_0,d13_pre_topc,d13_pre_topc,d5_pre_topc,d1_pre_topc,d5_pre_topc,d3_xboole_0,d7_xboole_0,t23_xboole_1,t16_xboole_1,t16_xboole_1,d7_xboole_0,d13_pre_topc,d3_tarski,t7_xboole_1,t49_pre_topc,t8_xboole_1,d10_xboole_0]),
    [file(pre_topc,t50_pre_topc),interesting(0.42)]).

fof(t51_pre_topc,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)))
             => r1_tarski(k6_pre_topc(A,k5_subset_1(u1_struct_0(A),B,C)),k5_subset_1(u1_struct_0(A),k6_pre_topc(A,B),k6_pre_topc(A,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t17_xboole_1,t49_pre_topc,t19_xboole_1]),
    [file(pre_topc,t51_pre_topc),interesting(0.42)]).

fof(t41_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ~ ( B != k1_pre_topc(A)
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ r2_hidden(C,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski]),
    [file(pre_topc,t41_pre_topc),interesting(0.40)]).

fof(t23_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ( ~ ( B != k2_pre_topc(A)
                & k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B) = k1_xboole_0 )
            & ~ ( k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B) != k1_xboole_0
                & B = k2_pre_topc(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t37_xboole_1,d10_xboole_0,t37_xboole_1]),
    [file(pre_topc,t23_pre_topc),interesting(0.28)]).

fof(t53_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ( ( v3_pre_topc(B,A)
             => k6_pre_topc(A,k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B)) = k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B) )
            & ( ( v2_pre_topc(A)
                & k6_pre_topc(A,k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B)) = k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B) )
             => v3_pre_topc(B,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t22_pre_topc,d6_pre_topc,t52_pre_topc,t52_pre_topc]),
    [file(pre_topc,t53_pre_topc),interesting(0.26)]).

fof(t18_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => k4_subset_1(u1_struct_0(A),B,k3_subset_1(u1_struct_0(A),B)) = k2_pre_topc(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_subset_1,d4_subset_1]),
    [file(pre_topc,t18_pre_topc),interesting(0.25)]).

fof(t46_pre_topc,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(k1_zfmisc_1(u1_struct_0(A))))
              & ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
                 => ( r2_hidden(D,C)
                  <=> ( v4_pre_topc(D,A)
                      & r1_tarski(B,D) ) ) )
              & k6_pre_topc(A,B) = k6_setfam_1(u1_struct_0(A),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s3_subset_1,t45_pre_topc,d1_setfam_1,d1_setfam_1,t45_pre_topc,t2_tarski]),
    [file(pre_topc,t46_pre_topc),interesting(0.14)]).

fof(t24_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(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)))
             => ( k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B) = C
               => k2_pre_topc(A) = k4_subset_1(u1_struct_0(A),B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_xboole_1]),
    [file(pre_topc,t24_pre_topc),interesting(0.08)]).

fof(t54_pre_topc,theorem,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r2_hidden(C,k6_pre_topc(A,B))
              <=> ( ~ v3_struct_0(A)
                  & ! [D] : 
                      ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A)))
                     => ~ ( v3_pre_topc(D,A)
                          & r2_hidden(C,D)
                          & r1_xboole_0(B,D) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d13_pre_topc,d1_struct_0,d1_struct_0,d13_pre_topc]),
    [file(pre_topc,t54_pre_topc),interesting(0.05)]).

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(t28_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => k3_xboole_0(A,B) = A ) ),
    file(xboole_1,t28_xboole_1),
    [interesting(0.00)]).

fof(t10_pre_topc,theorem,(
    $true ),
    file(pre_topc,t10_pre_topc),
    [interesting(0.00)]).

fof(t11_pre_topc,theorem,(
    $true ),
    file(pre_topc,t11_pre_topc),
    [interesting(0.00)]).

fof(t12_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => k2_pre_topc(A) = u1_struct_0(A) ) ),
    file(pre_topc,t12_pre_topc),
    [interesting(0.00)]).

fof(t13_pre_topc,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_struct_0(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => r2_hidden(B,k2_pre_topc(A)) ) ) ),
    file(pre_topc,t13_pre_topc),
    [interesting(0.00)]).

fof(t14_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => r1_tarski(B,k2_pre_topc(A)) ) ) ),
    file(pre_topc,t14_pre_topc),
    [interesting(0.00)]).

fof(t16_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( r1_tarski(B,k2_pre_topc(A))
         => m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ),
    file(pre_topc,t16_pre_topc),
    [interesting(0.00)]).

fof(t25_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => k4_subset_1(A,B,k3_subset_1(A,B)) = k2_subset_1(A) ) ),
    file(subset_1,t25_subset_1),
    [interesting(0.00)]).

fof(d4_subset_1,definition,(
    ! [A] : k2_subset_1(A) = A ),
    file(subset_1,d4_subset_1),
    [interesting(0.00)]).

fof(t19_pre_topc,theorem,(
    $true ),
    file(pre_topc,t19_pre_topc),
    [interesting(0.00)]).

fof(t1_pre_topc,theorem,(
    $true ),
    file(pre_topc,t1_pre_topc),
    [interesting(0.00)]).

fof(t20_pre_topc,theorem,(
    $true ),
    file(pre_topc,t20_pre_topc),
    [interesting(0.00)]).

fof(t21_pre_topc,theorem,(
    $true ),
    file(pre_topc,t21_pre_topc),
    [interesting(0.00)]).

fof(t45_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => B = k2_xboole_0(A,k4_xboole_0(B,A)) ) ),
    file(xboole_1,t45_xboole_1),
    [interesting(0.00)]).

fof(t40_xboole_1,theorem,(
    ! [A,B] : k4_xboole_0(k2_xboole_0(A,B),B) = k4_xboole_0(A,B) ),
    file(xboole_1,t40_xboole_1),
    [interesting(0.00)]).

fof(t83_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
    <=> k4_xboole_0(A,B) = A ) ),
    file(xboole_1,t83_xboole_1),
    [interesting(0.00)]).

fof(t25_pre_topc,theorem,(
    ! [A] : 
      ( l1_struct_0(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)))
             => ( ( k2_pre_topc(A) = k4_subset_1(u1_struct_0(A),B,C)
                  & r1_xboole_0(B,C) )
               => C = k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t40_xboole_1,t83_xboole_1]),
    [file(pre_topc,t25_pre_topc),interesting(0.00)]).

fof(t26_pre_topc,theorem,(
    $true ),
    file(pre_topc,t26_pre_topc),
    [interesting(0.00)]).

fof(t22_subset_1,theorem,(
    ! [A] : k2_subset_1(A) = k3_subset_1(A,k1_subset_1(A)) ),
    file(subset_1,t22_subset_1),
    [interesting(0.00)]).

fof(t28_pre_topc,theorem,(
    $true ),
    file(pre_topc,t28_pre_topc),
    [interesting(0.00)]).

fof(t29_pre_topc,theorem,(
    $true ),
    file(pre_topc,t29_pre_topc),
    [interesting(0.00)]).

fof(t2_pre_topc,theorem,(
    $true ),
    file(pre_topc,t2_pre_topc),
    [interesting(0.00)]).

fof(t30_pre_topc,theorem,(
    $true ),
    file(pre_topc,t30_pre_topc),
    [interesting(0.00)]).

fof(t31_pre_topc,theorem,(
    $true ),
    file(pre_topc,t31_pre_topc),
    [interesting(0.00)]).

fof(t32_pre_topc,theorem,(
    $true ),
    file(pre_topc,t32_pre_topc),
    [interesting(0.00)]).

fof(t33_pre_topc,theorem,(
    $true ),
    file(pre_topc,t33_pre_topc),
    [interesting(0.00)]).

fof(t34_pre_topc,theorem,(
    $true ),
    file(pre_topc,t34_pre_topc),
    [interesting(0.00)]).

fof(t35_pre_topc,theorem,(
    $true ),
    file(pre_topc,t35_pre_topc),
    [interesting(0.00)]).

fof(t36_pre_topc,theorem,(
    $true ),
    file(pre_topc,t36_pre_topc),
    [interesting(0.00)]).

fof(t37_pre_topc,theorem,(
    $true ),
    file(pre_topc,t37_pre_topc),
    [interesting(0.00)]).

fof(t38_pre_topc,theorem,(
    $true ),
    file(pre_topc,t38_pre_topc),
    [interesting(0.00)]).

fof(t3_pre_topc,theorem,(
    $true ),
    file(pre_topc,t3_pre_topc),
    [interesting(0.00)]).

fof(t40_pre_topc,theorem,(
    $true ),
    file(pre_topc,t40_pre_topc),
    [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(t37_xboole_1,theorem,(
    ! [A,B] : 
      ( k4_xboole_0(A,B) = k1_xboole_0
    <=> r1_tarski(A,B) ) ),
    file(xboole_1,t37_xboole_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(t2_xboole_1,theorem,(
    ! [A] : r1_tarski(k1_xboole_0,A) ),
    file(xboole_1,t2_xboole_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(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(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(d6_pre_topc,definition,(
    ! [A] : 
      ( l1_pre_topc(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ( v4_pre_topc(B,A)
          <=> v3_pre_topc(k6_subset_1(u1_struct_0(A),k2_pre_topc(A),B),A) ) ) ) ),
    file(pre_topc,d6_pre_topc),
    [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(t17_xboole_1,theorem,(
    ! [A,B] : r1_tarski(k3_xboole_0(A,B),A) ),
    file(xboole_1,t17_xboole_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(t48_xboole_1,theorem,(
    ! [A,B] : k4_xboole_0(A,k4_xboole_0(A,B)) = k3_xboole_0(A,B) ),
    file(xboole_1,t48_xboole_1),
    [interesting(0.00)]).

fof(d5_subset_1,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => k3_subset_1(A,B) = k4_xboole_0(A,B) ) ),
    file(subset_1,d5_subset_1),
    [interesting(0.00)]).

fof(t32_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => k6_subset_1(A,B,C) = k5_subset_1(A,B,k3_subset_1(A,C)) ) ) ),
    file(subset_1,t32_subset_1),
    [interesting(0.00)]).

fof(t47_xboole_1,theorem,(
    ! [A,B] : k4_xboole_0(A,k3_xboole_0(A,B)) = k4_xboole_0(A,B) ),
    file(xboole_1,t47_xboole_1),
    [interesting(0.00)]).

fof(d13_pre_topc,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(u1_struct_0(A)))
             => ( C = k6_pre_topc(A,B)
              <=> ! [D] : 
                    ( r2_hidden(D,u1_struct_0(A))
                   => ( r2_hidden(D,C)
                    <=> ! [E] : 
                          ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A)))
                         => ~ ( v3_pre_topc(E,A)
                              & r2_hidden(D,E)
                              & r1_xboole_0(B,E) ) ) ) ) ) ) ) ) ),
    file(pre_topc,d13_pre_topc),
    [interesting(0.00)]).

fof(t43_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( r1_xboole_0(B,C)
          <=> r1_tarski(B,k3_subset_1(A,C)) ) ) ) ),
    file(subset_1,t43_subset_1),
    [interesting(0.00)]).

fof(d4_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k4_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & ~ r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d4_xboole_0),
    [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(t2_tarski,theorem,(
    ! [A,B] : 
      ( ! [C] : 
          ( r2_hidden(C,A)
        <=> r2_hidden(C,B) )
     => A = B ) ),
    file(tarski,t2_tarski),
    [interesting(0.00)]).

fof(t4_pre_topc,theorem,(
    $true ),
    file(pre_topc,t4_pre_topc),
    [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(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(t23_xboole_1,theorem,(
    ! [A,B,C] : k3_xboole_0(A,k2_xboole_0(B,C)) = k2_xboole_0(k3_xboole_0(A,B),k3_xboole_0(A,C)) ),
    file(xboole_1,t23_xboole_1),
    [interesting(0.00)]).

fof(t16_xboole_1,theorem,(
    ! [A,B,C] : k3_xboole_0(k3_xboole_0(A,B),C) = k3_xboole_0(A,k3_xboole_0(B,C)) ),
    file(xboole_1,t16_xboole_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(t8_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(C,B) )
     => r1_tarski(k2_xboole_0(A,C),B) ) ),
    file(xboole_1,t8_xboole_1),
    [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(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(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(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(t6_pre_topc,theorem,(
    $true ),
    file(pre_topc,t6_pre_topc),
    [interesting(0.00)]).

fof(t7_pre_topc,theorem,(
    $true ),
    file(pre_topc,t7_pre_topc),
    [interesting(0.00)]).

fof(t8_pre_topc,theorem,(
    $true ),
    file(pre_topc,t8_pre_topc),
    [interesting(0.00)]).

fof(t9_pre_topc,theorem,(
    $true ),
    file(pre_topc,t9_pre_topc),
    [interesting(0.00)]).