fof(t11_setfam_1,theorem,(
    ! [A] : k1_setfam_1(k1_tarski(A)) = A ),
    inference(mizar_proof,[status(thm)],[d1_tarski,t4_setfam_1,d3_tarski,d1_tarski,d1_setfam_1,d10_xboole_0]),
    [file(setfam_1,t11_setfam_1),interesting(1.00)]).

fof(t8_setfam_1,theorem,(
    ! [A,B,C] : 
      ( ( r2_hidden(A,B)
        & r1_tarski(A,C) )
     => r1_tarski(k1_setfam_1(B),C) ) ),
    inference(mizar_proof,[status(thm)],[t4_setfam_1,t1_xboole_1]),
    [file(setfam_1,t8_setfam_1),interesting(0.87)]).

fof(t4_setfam_1,theorem,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => r1_tarski(k1_setfam_1(B),A) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d1_setfam_1]),
    [file(setfam_1,t4_setfam_1),interesting(0.86)]).

fof(t3_setfam_1,theorem,(
    ! [A] : r1_tarski(k1_setfam_1(A),k3_tarski(A)) ),
    inference(mizar_proof,[status(thm)],[d1_setfam_1,d4_tarski,d3_tarski,d1_setfam_1,t2_xboole_1]),
    [file(setfam_1,t3_setfam_1),interesting(0.83)]).

fof(t9_setfam_1,theorem,(
    ! [A,B,C] : 
      ( ( r2_hidden(A,B)
        & r1_xboole_0(A,C) )
     => r1_xboole_0(k1_setfam_1(B),C) ) ),
    inference(mizar_proof,[status(thm)],[t4_setfam_1,t63_xboole_1]),
    [file(setfam_1,t9_setfam_1),interesting(0.82)]).

fof(t5_setfam_1,theorem,(
    ! [A] : 
      ( r2_hidden(k1_xboole_0,A)
     => k1_setfam_1(A) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t4_setfam_1,t3_xboole_1]),
    [file(setfam_1,t5_setfam_1),interesting(0.81)]).

fof(t30_setfam_1,theorem,(
    ! [A] : r1_setfam_1(k3_setfam_1(A,A),A) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1,d5_setfam_1,t17_xboole_1]),
    [file(setfam_1,t30_setfam_1),interesting(0.75)]).

fof(t31_setfam_1,theorem,(
    ! [A] : r1_setfam_1(k4_setfam_1(A,A),A) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1,d6_setfam_1,t36_xboole_1]),
    [file(setfam_1,t31_setfam_1),interesting(0.75)]).

fof(t12_setfam_1,theorem,(
    ! [A,B] : k1_setfam_1(k2_tarski(A,B)) = k3_xboole_0(A,B) ),
    inference(mizar_proof,[status(thm)],[d2_tarski,d1_setfam_1,d2_tarski,d1_setfam_1,d3_xboole_0]),
    [file(setfam_1,t12_setfam_1),interesting(0.73)]).

fof(t29_setfam_1,theorem,(
    ! [A] : r1_setfam_1(A,k2_setfam_1(A,A)) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1,d4_setfam_1]),
    [file(setfam_1,t29_setfam_1),interesting(0.71)]).

fof(t17_setfam_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => r1_setfam_1(A,B) ) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1]),
    [file(setfam_1,t17_setfam_1),interesting(0.66)]).

fof(t20_setfam_1,theorem,(
    ! [A] : r1_setfam_1(k1_xboole_0,A) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1]),
    [file(setfam_1,t20_setfam_1),interesting(0.66)]).

fof(t2_setfam_1,theorem,(
    k1_setfam_1(k1_xboole_0) = k1_xboole_0 ),
    inference(mizar_proof,[status(thm)],[d1_setfam_1]),
    [file(setfam_1,t2_setfam_1),interesting(0.66)]).

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)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t58_setfam_1,t58_setfam_1]),
    [file(setfam_1,t59_setfam_1),interesting(0.64)]).

fof(t7_setfam_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => ( A = k1_xboole_0
        | r1_tarski(k1_setfam_1(B),k1_setfam_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d1_setfam_1,d1_setfam_1]),
    [file(setfam_1,t7_setfam_1),interesting(0.63)]).

fof(t53_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)))
         => ( k7_setfam_1(A,B) = k7_setfam_1(A,C)
           => B = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[t51_setfam_1,t51_setfam_1,d10_xboole_0]),
    [file(setfam_1,t53_setfam_1),interesting(0.63)]).

fof(t23_setfam_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_setfam_1(A,B)
        & r1_setfam_1(B,C) )
     => r1_setfam_1(A,C) ) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1,d2_setfam_1,t1_xboole_1]),
    [file(setfam_1,t23_setfam_1),interesting(0.62)]).

fof(t41_setfam_1,theorem,(
    ! [A,B] : r1_tarski(k1_setfam_1(k4_setfam_1(A,B)),k4_xboole_0(k1_setfam_1(A),k1_setfam_1(B))) ),
    inference(mizar_proof,[status(thm)],[d1_xboole_0,d6_setfam_1,d1_setfam_1,t2_xboole_1,d6_setfam_1,d3_tarski,d6_setfam_1,d1_setfam_1,d4_xboole_0,d1_setfam_1,d1_setfam_1,d4_xboole_0,d1_setfam_1,d4_xboole_0]),
    [file(setfam_1,t41_setfam_1),interesting(0.60)]).

fof(t52_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(k7_setfam_1(A,B),C)
          <=> r1_tarski(B,k7_setfam_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t51_setfam_1,t51_setfam_1]),
    [file(setfam_1,t52_setfam_1),interesting(0.60)]).

fof(t18_setfam_1,theorem,(
    ! [A,B] : 
      ( r1_setfam_1(A,B)
     => r1_tarski(k3_tarski(A),k3_tarski(B)) ) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1,d3_tarski,d4_tarski,d4_tarski]),
    [file(setfam_1,t18_setfam_1),interesting(0.59)]).

fof(t56_setfam_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(k3_tarski(A),B)
        & r2_hidden(C,A) )
     => r1_tarski(C,B) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d4_tarski]),
    [file(setfam_1,t56_setfam_1),interesting(0.56)]).

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)) ) ),
    inference(mizar_proof,[status(thm)],[t15_xboole_1,t7_xboole_1,t7_setfam_1,t19_xboole_1,d3_tarski,d3_xboole_0,d2_xboole_0,d1_setfam_1,d1_setfam_1,d10_xboole_0]),
    [file(setfam_1,t10_setfam_1),interesting(0.55)]).

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) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_setfam_1,d1_setfam_1,d1_setfam_1,d10_setfam_1,d10_setfam_1]),
    [file(setfam_1,t58_setfam_1),interesting(0.55)]).

fof(t39_setfam_1,theorem,(
    ! [A,B] : k3_tarski(k3_setfam_1(A,B)) = k3_xboole_0(k3_tarski(A),k3_tarski(B)) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d4_tarski,d5_setfam_1,d3_xboole_0,d4_tarski,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,d4_tarski,d4_tarski,d5_setfam_1,d3_xboole_0,d4_tarski]),
    [file(setfam_1,t39_setfam_1),interesting(0.54)]).

fof(t36_setfam_1,theorem,(
    ! [A,B] : k3_xboole_0(A,k3_tarski(B)) = k3_tarski(k3_setfam_1(k1_tarski(A),B)) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d4_tarski,d1_tarski,d5_setfam_1,d3_xboole_0,d4_tarski,d3_tarski,d4_tarski,d5_setfam_1,d1_tarski,d3_xboole_0,d4_tarski,d3_xboole_0,d10_xboole_0]),
    [file(setfam_1,t36_setfam_1),interesting(0.52)]).

fof(t25_setfam_1,theorem,(
    ! [A,B,C] : 
      ( r1_setfam_1(C,k2_tarski(A,B))
     => ! [D] : ~ ( r2_hidden(D,C)
          & ~ r1_tarski(D,A)
          & ~ r1_tarski(D,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1,t41_enumset1,d2_xboole_0,d1_tarski]),
    [file(setfam_1,t25_setfam_1),interesting(0.51)]).

fof(t21_setfam_1,theorem,(
    ! [A] : 
      ( r1_setfam_1(A,k1_xboole_0)
     => A = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1]),
    [file(setfam_1,t21_setfam_1),interesting(0.50)]).

fof(t24_setfam_1,theorem,(
    ! [A,B] : 
      ( r1_setfam_1(B,k1_tarski(A))
     => ! [C] : 
          ( r2_hidden(C,B)
         => r1_tarski(C,A) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_setfam_1,d1_tarski]),
    [file(setfam_1,t24_setfam_1),interesting(0.49)]).

fof(t34_setfam_1,theorem,(
    ! [A,B] : 
      ( ~ r1_xboole_0(A,B)
     => k3_xboole_0(k1_setfam_1(A),k1_setfam_1(B)) = k1_setfam_1(k3_setfam_1(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d7_xboole_0,d3_xboole_0,d5_setfam_1,d3_tarski,d3_xboole_0,d5_setfam_1,d1_setfam_1,d3_xboole_0,d1_setfam_1,d3_tarski,d5_setfam_1,d1_setfam_1,d3_xboole_0,d1_setfam_1,d5_setfam_1,d1_setfam_1,d3_xboole_0,d1_setfam_1,d3_xboole_0,d10_xboole_0]),
    [file(setfam_1,t34_setfam_1),interesting(0.49)]).

fof(t19_setfam_1,theorem,(
    ! [A,B] : 
      ( r2_setfam_1(B,A)
     => ( A = k1_xboole_0
        | r1_tarski(k1_setfam_1(B),k1_setfam_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_setfam_1,d3_tarski,d1_setfam_1,d1_setfam_1]),
    [file(setfam_1,t19_setfam_1),interesting(0.48)]).

fof(t46_setfam_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ~ ( B != k1_xboole_0
          & k7_setfam_1(A,B) = k1_xboole_0 ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d8_setfam_1]),
    [file(setfam_1,t46_setfam_1),interesting(0.47)]).

fof(t6_setfam_1,theorem,(
    ! [A,B] : 
      ( ! [C] : 
          ( r2_hidden(C,A)
         => r1_tarski(B,C) )
     => ( A = k1_xboole_0
        | r1_tarski(B,k1_setfam_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d1_setfam_1]),
    [file(setfam_1,t6_setfam_1),interesting(0.47)]).

fof(t51_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(k7_setfam_1(A,B),k7_setfam_1(A,C))
           => r1_tarski(B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d8_setfam_1,d8_setfam_1]),
    [file(setfam_1,t51_setfam_1),interesting(0.44)]).

fof(t57_setfam_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(C,k3_tarski(k2_xboole_0(A,B)))
        & ! [D] : 
            ( r2_hidden(D,B)
           => r1_xboole_0(D,C) ) )
     => r1_tarski(C,k3_tarski(A)) ) ),
    inference(mizar_proof,[status(thm)],[t98_zfmisc_1,d7_xboole_0,t19_xboole_1,t96_zfmisc_1,t23_xboole_1,t17_xboole_1,t1_xboole_1]),
    [file(setfam_1,t57_setfam_1),interesting(0.43)]).

fof(t35_setfam_1,theorem,(
    ! [A,B] : 
      ( B != k1_xboole_0
     => k2_xboole_0(A,k1_setfam_1(B)) = k1_setfam_1(k2_setfam_1(k1_tarski(A),B)) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d4_setfam_1,d3_tarski,d2_xboole_0,d4_setfam_1,d1_setfam_1,d1_tarski,d2_xboole_0,d1_setfam_1,d3_tarski,d2_xboole_0,d1_setfam_1,d1_tarski,d4_setfam_1,d1_setfam_1,d2_xboole_0,d10_xboole_0]),
    [file(setfam_1,t35_setfam_1),interesting(0.38)]).

fof(t37_setfam_1,theorem,(
    ! [A,B] : 
      ( B != k1_xboole_0
     => k4_xboole_0(A,k3_tarski(B)) = k1_setfam_1(k4_setfam_1(k1_tarski(A),B)) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d6_setfam_1,d3_tarski,d4_xboole_0,d6_setfam_1,d1_tarski,d4_tarski,d4_xboole_0,d1_setfam_1,d3_tarski,d1_setfam_1,d4_xboole_0,d6_setfam_1,d1_setfam_1,d4_xboole_0,d4_tarski,d4_xboole_0,d10_xboole_0]),
    [file(setfam_1,t37_setfam_1),interesting(0.34)]).

fof(t38_setfam_1,theorem,(
    ! [A,B] : 
      ( B != k1_xboole_0
     => k4_xboole_0(A,k1_setfam_1(B)) = k3_tarski(k4_setfam_1(k1_tarski(A),B)) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d3_tarski,d4_xboole_0,d1_setfam_1,d6_setfam_1,d4_xboole_0,d4_tarski,d3_tarski,d4_tarski,d6_setfam_1,d1_tarski,d4_xboole_0,d1_setfam_1,d4_xboole_0,d10_xboole_0]),
    [file(setfam_1,t38_setfam_1),interesting(0.34)]).

fof(t49_setfam_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( r2_hidden(k3_subset_1(A,C),k7_setfam_1(A,B))
          <=> r2_hidden(C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_setfam_1]),
    [file(setfam_1,t49_setfam_1),interesting(0.25)]).

fof(t40_setfam_1,theorem,(
    ! [A,B] : ~ ( A != k1_xboole_0
      & B != k1_xboole_0
      & ~ r1_tarski(k2_xboole_0(k1_setfam_1(A),k1_setfam_1(B)),k1_setfam_1(k2_setfam_1(A,B))) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d2_xboole_0,d4_setfam_1,d1_setfam_1,d2_xboole_0,d4_setfam_1,d1_setfam_1]),
    [file(setfam_1,t40_setfam_1),interesting(0.23)]).

fof(t55_setfam_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( B = k1_tarski(A)
       => k7_setfam_1(A,B) = k1_tarski(k1_xboole_0) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_xboole_1,t37_zfmisc_1,d1_tarski,t22_subset_1,d4_subset_1,d1_tarski,d1_tarski,d4_subset_1,t21_subset_1,d1_tarski,d8_setfam_1]),
    [file(setfam_1,t55_setfam_1),interesting(0.23)]).

fof(t44_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)))
         => ( ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ( r2_hidden(D,B)
                <=> r2_hidden(D,C) ) )
           => B = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d10_xboole_0,d3_tarski]),
    [file(setfam_1,t44_setfam_1),interesting(0.22)]).

fof(t47_setfam_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( B != k1_xboole_0
       => k6_subset_1(A,k2_subset_1(A),k5_setfam_1(A,B)) = k6_setfam_1(A,k7_setfam_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_setfam_1,d8_setfam_1,d5_subset_1,d4_xboole_0,d8_setfam_1,d5_subset_1,d4_xboole_0,d3_tarski,d4_xboole_0,d4_tarski,d1_setfam_1,d3_tarski,d1_setfam_1,d4_tarski,d4_subset_1,d4_xboole_0,d10_xboole_0]),
    [file(setfam_1,t47_setfam_1),interesting(0.17)]).

fof(t54_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)))
         => k7_setfam_1(A,k4_subset_1(k1_zfmisc_1(A),B,C)) = k4_subset_1(k1_zfmisc_1(A),k7_setfam_1(A,B),k7_setfam_1(A,C)) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_setfam_1,d2_xboole_0,d8_setfam_1]),
    [file(setfam_1,t54_setfam_1),interesting(0.08)]).

fof(t15_xboole_1,theorem,(
    ! [A,B] : 
      ( k2_xboole_0(A,B) = k1_xboole_0
     => A = k1_xboole_0 ) ),
    file(xboole_1,t15_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(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(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(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(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(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(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(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [interesting(0.00)]).

fof(d2_tarski,definition,(
    ! [A,B,C] : 
      ( C = k2_tarski(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( D = A
            | D = B ) ) ) ),
    file(tarski,d2_tarski),
    [interesting(0.00)]).

fof(t13_setfam_1,theorem,(
    $true ),
    file(setfam_1,t13_setfam_1),
    [interesting(0.00)]).

fof(t14_setfam_1,theorem,(
    $true ),
    file(setfam_1,t14_setfam_1),
    [interesting(0.00)]).

fof(t15_setfam_1,theorem,(
    $true ),
    file(setfam_1,t15_setfam_1),
    [interesting(0.00)]).

fof(t16_setfam_1,theorem,(
    $true ),
    file(setfam_1,t16_setfam_1),
    [interesting(0.00)]).

fof(d2_setfam_1,definition,(
    ! [A,B] : 
      ( r1_setfam_1(A,B)
    <=> ! [C] : ~ ( r2_hidden(C,A)
          & ! [D] : ~ ( r2_hidden(D,B)
              & r1_tarski(C,D) ) ) ) ),
    file(setfam_1,d2_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(d3_setfam_1,definition,(
    ! [A,B] : 
      ( r2_setfam_1(A,B)
    <=> ! [C] : ~ ( r2_hidden(C,B)
          & ! [D] : ~ ( r2_hidden(D,A)
              & r1_tarski(D,C) ) ) ) ),
    file(setfam_1,d3_setfam_1),
    [interesting(0.00)]).

fof(t1_setfam_1,theorem,(
    $true ),
    file(setfam_1,t1_setfam_1),
    [interesting(0.00)]).

fof(t22_setfam_1,theorem,(
    $true ),
    file(setfam_1,t22_setfam_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(t41_enumset1,theorem,(
    ! [A,B] : k2_tarski(A,B) = k2_xboole_0(k1_tarski(A),k1_tarski(B)) ),
    file(enumset1,t41_enumset1),
    [interesting(0.00)]).

fof(t26_setfam_1,theorem,(
    $true ),
    file(setfam_1,t26_setfam_1),
    [interesting(0.00)]).

fof(t27_setfam_1,theorem,(
    $true ),
    file(setfam_1,t27_setfam_1),
    [interesting(0.00)]).

fof(t28_setfam_1,theorem,(
    $true ),
    file(setfam_1,t28_setfam_1),
    [interesting(0.00)]).

fof(d4_setfam_1,definition,(
    ! [A,B,C] : 
      ( C = k2_setfam_1(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ? [E,F] : 
              ( r2_hidden(E,A)
              & r2_hidden(F,B)
              & D = k2_xboole_0(E,F) ) ) ) ),
    file(setfam_1,d4_setfam_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(t17_xboole_1,theorem,(
    ! [A,B] : r1_tarski(k3_xboole_0(A,B),A) ),
    file(xboole_1,t17_xboole_1),
    [interesting(0.00)]).

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

fof(t36_xboole_1,theorem,(
    ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ),
    file(xboole_1,t36_xboole_1),
    [interesting(0.00)]).

fof(t32_setfam_1,theorem,(
    $true ),
    file(setfam_1,t32_setfam_1),
    [interesting(0.00)]).

fof(t33_setfam_1,theorem,(
    $true ),
    file(setfam_1,t33_setfam_1),
    [interesting(0.00)]).

fof(d7_xboole_0,definition,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
    <=> k3_xboole_0(A,B) = k1_xboole_0 ) ),
    file(xboole_0,d7_xboole_0),
    [interesting(0.00)]).

fof(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(t2_xboole_1,theorem,(
    ! [A] : r1_tarski(k1_xboole_0,A) ),
    file(xboole_1,t2_xboole_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(t42_setfam_1,theorem,(
    $true ),
    file(setfam_1,t42_setfam_1),
    [interesting(0.00)]).

fof(t43_setfam_1,theorem,(
    $true ),
    file(setfam_1,t43_setfam_1),
    [interesting(0.00)]).

fof(t45_setfam_1,theorem,(
    $true ),
    file(setfam_1,t45_setfam_1),
    [interesting(0.00)]).

fof(d8_setfam_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 = k7_setfam_1(A,B)
          <=> ! [D] : 
                ( m1_subset_1(D,k1_zfmisc_1(A))
               => ( r2_hidden(D,C)
                <=> r2_hidden(k3_subset_1(A,D),B) ) ) ) ) ) ),
    file(setfam_1,d8_setfam_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(d4_subset_1,definition,(
    ! [A] : k2_subset_1(A) = A ),
    file(subset_1,d4_subset_1),
    [interesting(0.00)]).

fof(t48_setfam_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
     => ( B != k1_xboole_0
       => k5_setfam_1(A,k7_setfam_1(A,B)) = k6_subset_1(A,k2_subset_1(A),k6_setfam_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d4_tarski,d4_subset_1,d8_setfam_1,d5_subset_1,d4_xboole_0,d1_setfam_1,d4_xboole_0,d3_tarski,d4_xboole_0,d1_setfam_1,d5_subset_1,d8_setfam_1,d4_xboole_0,d4_tarski,d10_xboole_0]),
    [file(setfam_1,t48_setfam_1),interesting(0.00)]).

fof(t50_setfam_1,theorem,(
    $true ),
    file(setfam_1,t50_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(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(t21_subset_1,theorem,(
    ! [A] : k1_subset_1(A) = k3_subset_1(A,k2_subset_1(A)) ),
    file(subset_1,t21_subset_1),
    [interesting(0.00)]).

fof(t98_zfmisc_1,theorem,(
    ! [A,B] : 
      ( ! [C] : 
          ( r2_hidden(C,A)
         => r1_xboole_0(C,B) )
     => r1_xboole_0(k3_tarski(A),B) ) ),
    file(zfmisc_1,t98_zfmisc_1),
    [interesting(0.00)]).

fof(t96_zfmisc_1,theorem,(
    ! [A,B] : k3_tarski(k2_xboole_0(A,B)) = k2_xboole_0(k3_tarski(A),k3_tarski(B)) ),
    file(zfmisc_1,t96_zfmisc_1),
    [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(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(t3_xboole_1,theorem,(
    ! [A] : 
      ( r1_tarski(A,k1_xboole_0)
     => A = k1_xboole_0 ) ),
    file(xboole_1,t3_xboole_1),
    [interesting(0.00)]).

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