fof(t20_finsub_1,theorem,(
    ! [A] : v4_finsub_1(k1_zfmisc_1(A)) ),
    inference(mizar_proof,[status(thm)],[t10_finsub_1]),
    [file(finsub_1,t20_finsub_1),interesting(1.00)]).

fof(t27_finsub_1,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => k5_finsub_1(A) = k1_zfmisc_1(A) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t13_finset_1,d5_finsub_1,t26_finsub_1,d10_xboole_0]),
    [file(finsub_1,t27_finsub_1),interesting(0.80)]).

fof(t23_finsub_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => r1_tarski(k5_finsub_1(A),k5_finsub_1(B)) ) ),
    inference(mizar_proof,[status(thm)],[d5_finsub_1,t1_xboole_1,d5_finsub_1,d3_tarski]),
    [file(finsub_1,t23_finsub_1),interesting(0.74)]).

fof(t26_finsub_1,theorem,(
    ! [A] : r1_tarski(k5_finsub_1(A),k1_zfmisc_1(A)) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d5_finsub_1]),
    [file(finsub_1,t26_finsub_1),interesting(0.74)]).

fof(t24_finsub_1,theorem,(
    ! [A,B] : k5_finsub_1(k3_xboole_0(A,B)) = k3_xboole_0(k5_finsub_1(A),k5_finsub_1(B)) ),
    inference(mizar_proof,[status(thm)],[t17_xboole_1,t23_finsub_1,t19_xboole_1,d10_xboole_0,d3_xboole_0,d5_finsub_1,t19_xboole_1,d5_finsub_1,d3_tarski]),
    [file(finsub_1,t24_finsub_1),interesting(0.63)]).

fof(t28_finsub_1,theorem,(
    k5_finsub_1(k1_xboole_0) = k1_tarski(k1_xboole_0) ),
    inference(mizar_proof,[status(thm)],[t27_finsub_1,t1_zfmisc_1]),
    [file(finsub_1,t28_finsub_1),interesting(0.60)]).

fof(t21_finsub_1,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v4_finsub_1(A) )
     => ! [B] : 
          ( ( ~ v1_xboole_0(B)
            & v4_finsub_1(B) )
         => ( ~ v1_xboole_0(k3_xboole_0(A,B))
            & v4_finsub_1(k3_xboole_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_finsub_1,d3_xboole_0,d3_xboole_0,t10_finsub_1,d3_xboole_0,t10_finsub_1,d3_xboole_0,t10_finsub_1]),
    [file(finsub_1,t21_finsub_1),interesting(0.58)]).

fof(t25_finsub_1,theorem,(
    ! [A,B] : r1_tarski(k2_xboole_0(k5_finsub_1(A),k5_finsub_1(B)),k5_finsub_1(k2_xboole_0(A,B))) ),
    inference(mizar_proof,[status(thm)],[t7_xboole_1,t23_finsub_1,t8_xboole_1]),
    [file(finsub_1,t25_finsub_1),interesting(0.53)]).

fof(t18_finsub_1,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v4_finsub_1(A) )
     => r2_hidden(k1_xboole_0,A) ) ),
    inference(mizar_proof,[status(thm)],[t37_xboole_1]),
    [file(finsub_1,t18_finsub_1),interesting(0.51)]).

fof(t32_finsub_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k5_finsub_1(A))
     => m1_subset_1(B,k1_zfmisc_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[d5_finsub_1]),
    [file(finsub_1,t32_finsub_1),interesting(0.46)]).

fof(t10_finsub_1,theorem,(
    ! [A] : 
      ( v4_finsub_1(A)
    <=> ! [B,C] : 
          ( ( r2_hidden(B,A)
            & r2_hidden(C,A) )
         => ( r2_hidden(k2_xboole_0(B,C),A)
            & r2_hidden(k4_xboole_0(B,C),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_finsub_1,d1_finsub_1,d3_finsub_1,d1_finsub_1,d3_finsub_1,d4_finsub_1]),
    [file(finsub_1,t10_finsub_1),interesting(0.42)]).

fof(t34_finsub_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ( v1_finset_1(A)
       => m1_subset_1(B,k5_finsub_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t13_finset_1,d5_finsub_1]),
    [file(finsub_1,t34_finsub_1),interesting(0.36)]).

fof(t13_finsub_1,theorem,(
    ! [A,B,C] : 
      ( ( ~ v1_xboole_0(C)
        & v4_finsub_1(C) )
     => ( ( m1_subset_1(A,C)
          & m1_subset_1(B,C) )
       => m1_subset_1(k3_xboole_0(A,B),C) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_xboole_1]),
    [file(finsub_1,t13_finsub_1),interesting(0.26)]).

fof(t16_finsub_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( m1_subset_1(B,A)
           => ! [C] : 
                ( m1_subset_1(C,A)
               => ( r2_hidden(k5_xboole_0(B,C),A)
                  & r2_hidden(k3_xboole_0(B,C),A) ) ) )
       => v4_finsub_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t94_xboole_1,t100_xboole_1,t10_finsub_1]),
    [file(finsub_1,t16_finsub_1),interesting(0.04)]).

fof(t17_finsub_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( m1_subset_1(B,A)
           => ! [C] : 
                ( m1_subset_1(C,A)
               => ( r2_hidden(k5_xboole_0(B,C),A)
                  & r2_hidden(k2_xboole_0(B,C),A) ) ) )
       => v4_finsub_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t95_xboole_1,t100_xboole_1,t10_finsub_1]),
    [file(finsub_1,t17_finsub_1),interesting(0.04)]).

fof(t11_finsub_1,theorem,(
    $true ),
    file(finsub_1,t11_finsub_1),
    [interesting(0.00)]).

fof(t12_finsub_1,theorem,(
    $true ),
    file(finsub_1,t12_finsub_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(t14_finsub_1,theorem,(
    ! [A,B,C] : 
      ( ( ~ v1_xboole_0(C)
        & v4_finsub_1(C) )
     => ( ( m1_subset_1(A,C)
          & m1_subset_1(B,C) )
       => m1_subset_1(k5_xboole_0(A,B),C) ) ) ),
    file(finsub_1,t14_finsub_1),
    [interesting(0.00)]).

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

fof(d4_finsub_1,definition,(
    ! [A] : 
      ( v4_finsub_1(A)
    <=> ( v1_finsub_1(A)
        & v3_finsub_1(A) ) ) ),
    file(finsub_1,d4_finsub_1),
    [interesting(0.00)]).

fof(d1_finsub_1,definition,(
    ! [A] : 
      ( v1_finsub_1(A)
    <=> ! [B,C] : 
          ( ( r2_hidden(B,A)
            & r2_hidden(C,A) )
         => r2_hidden(k2_xboole_0(B,C),A) ) ) ),
    file(finsub_1,d1_finsub_1),
    [interesting(0.00)]).

fof(d3_finsub_1,definition,(
    ! [A] : 
      ( v3_finsub_1(A)
    <=> ! [B,C] : 
          ( ( r2_hidden(B,A)
            & r2_hidden(C,A) )
         => r2_hidden(k4_xboole_0(B,C),A) ) ) ),
    file(finsub_1,d3_finsub_1),
    [interesting(0.00)]).

fof(t15_finsub_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( m1_subset_1(B,A)
           => ! [C] : 
                ( m1_subset_1(C,A)
               => ( r2_hidden(k5_xboole_0(B,C),A)
                  & r2_hidden(k4_xboole_0(B,C),A) ) ) )
       => v4_finsub_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t98_xboole_1,t10_finsub_1]),
    [file(finsub_1,t15_finsub_1),interesting(0.00)]).

fof(t94_xboole_1,theorem,(
    ! [A,B] : k2_xboole_0(A,B) = k5_xboole_0(k5_xboole_0(A,B),k3_xboole_0(A,B)) ),
    file(xboole_1,t94_xboole_1),
    [interesting(0.00)]).

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

fof(t95_xboole_1,theorem,(
    ! [A,B] : k3_xboole_0(A,B) = k5_xboole_0(k5_xboole_0(A,B),k2_xboole_0(A,B)) ),
    file(xboole_1,t95_xboole_1),
    [interesting(0.00)]).

fof(t19_finsub_1,theorem,(
    $true ),
    file(finsub_1,t19_finsub_1),
    [interesting(0.00)]).

fof(t1_finsub_1,theorem,(
    $true ),
    file(finsub_1,t1_finsub_1),
    [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(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(t22_finsub_1,theorem,(
    $true ),
    file(finsub_1,t22_finsub_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(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(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(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(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(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(t13_finset_1,theorem,(
    ! [A,B] : 
      ( ( r1_tarski(A,B)
        & v1_finset_1(B) )
     => v1_finset_1(A) ) ),
    file(finset_1,t13_finset_1),
    [interesting(0.00)]).

fof(t1_zfmisc_1,theorem,(
    k1_zfmisc_1(k1_xboole_0) = k1_tarski(k1_xboole_0) ),
    file(zfmisc_1,t1_zfmisc_1),
    [interesting(0.00)]).

fof(t29_finsub_1,theorem,(
    $true ),
    file(finsub_1,t29_finsub_1),
    [interesting(0.00)]).

fof(t2_finsub_1,theorem,(
    $true ),
    file(finsub_1,t2_finsub_1),
    [interesting(0.00)]).

fof(t30_finsub_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k5_finsub_1(A))
     => v1_finset_1(B) ) ),
    file(finsub_1,t30_finsub_1),
    [interesting(0.00)]).

fof(t31_finsub_1,theorem,(
    $true ),
    file(finsub_1,t31_finsub_1),
    [interesting(0.00)]).

fof(t33_finsub_1,theorem,(
    $true ),
    file(finsub_1,t33_finsub_1),
    [interesting(0.00)]).

fof(t3_finsub_1,theorem,(
    $true ),
    file(finsub_1,t3_finsub_1),
    [interesting(0.00)]).

fof(t4_finsub_1,theorem,(
    $true ),
    file(finsub_1,t4_finsub_1),
    [interesting(0.00)]).

fof(t5_finsub_1,theorem,(
    $true ),
    file(finsub_1,t5_finsub_1),
    [interesting(0.00)]).

fof(t6_finsub_1,theorem,(
    $true ),
    file(finsub_1,t6_finsub_1),
    [interesting(0.00)]).

fof(t7_finsub_1,theorem,(
    $true ),
    file(finsub_1,t7_finsub_1),
    [interesting(0.00)]).

fof(t8_finsub_1,theorem,(
    $true ),
    file(finsub_1,t8_finsub_1),
    [interesting(0.00)]).

fof(t9_finsub_1,theorem,(
    $true ),
    file(finsub_1,t9_finsub_1),
    [interesting(0.00)]).