fof(t12_realset1,theorem,(
    ! [A] : 
      ( ~ v1_realset1(A)
     => ! [B] : 
          ( m4_realset1(B,A)
         => ~ v1_xboole_0(k4_xboole_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_realset1,t4_realset1]),
    [file(realset1,t12_realset1),interesting(1.00)]).

fof(t4_realset1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ~ v1_realset1(A)
      <=> ! [B] : ~ v1_xboole_0(k4_xboole_0(A,k1_tarski(B))) ) ) ),
    inference(mizar_proof,[status(thm)],[t41_zfmisc_1,d1_tarski,d4_xboole_0,d4_realset1,t37_xboole_1]),
    [file(realset1,t4_realset1),interesting(0.87)]).

fof(t5_realset1,theorem,(
    ? [A] : 
      ( ~ v1_xboole_0(A)
      & ! [B] : 
          ( m1_subset_1(B,A)
         => ~ v1_xboole_0(k4_xboole_0(A,k1_tarski(B))) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_tarski,d1_tarski,d4_xboole_0,d2_tarski,d1_tarski,d4_xboole_0,d2_tarski]),
    [file(realset1,t5_realset1),interesting(0.79)]).

fof(t13_realset1,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ( v1_realset1(A)
      <=> ~ r1_xreal_0(2,k4_card_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_realset1,t78_card_1,t79_card_1,t59_card_2,d4_realset1,t60_card_2,d4_realset1,t71_nat_1]),
    [file(realset1,t13_realset1),interesting(0.75)]).

fof(t14_realset1,theorem,(
    ! [A] : 
      ( ~ ( ~ v1_realset1(A)
          & ! [B,C] : ~ ( r2_hidden(B,A)
              & r2_hidden(C,A)
              & B != C ) )
      & ~ ( ? [B,C] : 
              ( r2_hidden(B,A)
              & r2_hidden(C,A)
              & B != C )
          & v1_realset1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_realset1,d1_xboole_0,t41_zfmisc_1,d4_realset1,t38_zfmisc_1,t26_zfmisc_1]),
    [file(realset1,t14_realset1),interesting(0.75)]).

fof(t15_realset1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ( ~ ( ~ v1_realset1(B)
            & ! [C] : 
                ( m1_subset_1(C,A)
               => ! [D] : 
                    ( m1_subset_1(D,A)
                   => ~ ( r2_hidden(C,B)
                        & r2_hidden(D,B)
                        & C != D ) ) ) )
        & ~ ( ? [C] : 
                ( m1_subset_1(C,A)
                & ? [D] : 
                    ( m1_subset_1(D,A)
                    & r2_hidden(C,B)
                    & r2_hidden(D,B)
                    & C != D ) )
            & v1_realset1(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_realset1,t14_realset1]),
    [file(realset1,t15_realset1),interesting(0.73)]).

fof(t7_realset1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ( ! [B] : 
            ( m1_subset_1(B,A)
           => ~ v1_xboole_0(k4_xboole_0(A,k1_tarski(B))) )
       => ~ v1_realset1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_realset1]),
    [file(realset1,t7_realset1),interesting(0.73)]).

fof(t1_realset1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,k2_zfmisc_1(A,A),A)
        & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
     => ( r2_hidden(B,k2_zfmisc_1(A,A))
       => r2_hidden(k1_funct_1(C,B),A) ) ) ),
    inference(mizar_proof,[status(thm)],[t113_zfmisc_1,d1_funct_2,t12_relset_1,d5_funct_1]),
    [file(realset1,t1_realset1),interesting(0.71)]).

fof(t6_realset1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ~ ( ! [B] : 
              ( m1_subset_1(B,A)
             => ~ v1_xboole_0(k4_xboole_0(A,k1_tarski(B))) )
          & v1_realset1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_realset1,d1_tarski,t37_xboole_1]),
    [file(realset1,t6_realset1),interesting(0.70)]).

fof(t2_realset1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k2_zfmisc_1(A,A),A)
        & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
     => ? [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
          & ! [D] : 
              ( r2_hidden(D,k2_zfmisc_1(C,C))
             => r2_hidden(k1_funct_1(B,D),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_realset1]),
    [file(realset1,t2_realset1),interesting(0.61)]).

fof(t9_realset1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m2_realset1(C,A,B)
         => ( v1_funct_1(k1_realset1(C,B))
            & v1_funct_2(k1_realset1(C,B),k2_zfmisc_1(B,B),B)
            & m2_relset_1(k1_realset1(C,B),k2_zfmisc_1(B,B),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t113_zfmisc_1,d1_funct_2,t12_relset_1,t119_zfmisc_1,t91_relat_1,t70_funct_1,d6_realset1,t5_funct_2]),
    [file(realset1,t9_realset1),interesting(0.58)]).

fof(t8_realset1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ? [C] : 
          ( v1_funct_1(C)
          & v1_funct_2(C,k2_zfmisc_1(A,A),A)
          & m2_relset_1(C,k2_zfmisc_1(A,A),A)
          & ! [D] : 
              ( r2_hidden(D,k2_zfmisc_1(B,B))
             => r2_hidden(k1_funct_1(C,D),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_zfmisc_1,d5_funct_3]),
    [file(realset1,t8_realset1),interesting(0.55)]).

fof(t3_realset1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k2_zfmisc_1(A,A),A)
        & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
     => ! [C] : 
          ( m1_realset1(C,A,B)
         => ( v1_funct_1(k1_realset1(B,C))
            & v1_funct_2(k1_realset1(B,C),k2_zfmisc_1(C,C),C)
            & m2_relset_1(k1_realset1(B,C),k2_zfmisc_1(C,C),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t113_zfmisc_1,d1_funct_2,t12_relset_1,t119_zfmisc_1,t91_relat_1,t70_funct_1,d2_realset1,t5_funct_2]),
    [file(realset1,t3_realset1),interesting(0.53)]).

fof(t10_realset1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,A)
     => ? [C] : 
          ( v1_funct_1(C)
          & v1_funct_2(C,k2_zfmisc_1(A,A),A)
          & m2_relset_1(C,k2_zfmisc_1(A,A),A)
          & ! [D] : 
              ( r2_hidden(D,k2_zfmisc_1(k4_xboole_0(A,k1_tarski(B)),k4_xboole_0(A,k1_tarski(B))))
             => r2_hidden(k1_funct_1(C,D),k4_xboole_0(A,k1_tarski(B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t36_xboole_1,t8_realset1]),
    [file(realset1,t10_realset1),interesting(0.34)]).

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(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(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(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_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(t91_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r1_tarski(A,k1_relat_1(B))
       => k1_relat_1(k7_relat_1(B,A)) = A ) ) ),
    file(relat_1,t91_relat_1),
    [interesting(0.00)]).

fof(t70_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,k1_relat_1(k7_relat_1(C,A)))
       => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t70_funct_1),
    [interesting(0.00)]).

fof(d8_realset1,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,A)
     => ! [C] : 
          ( ( v1_funct_1(C)
            & v1_funct_2(C,k2_zfmisc_1(A,A),A)
            & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
         => ( m3_realset1(C,A,B)
          <=> ! [D] : 
                ( r2_hidden(D,k2_zfmisc_1(k4_xboole_0(A,k1_tarski(B)),k4_xboole_0(A,k1_tarski(B))))
               => r2_hidden(k1_funct_1(C,D),k4_xboole_0(A,k1_tarski(B))) ) ) ) ) ),
    file(realset1,d8_realset1),
    [interesting(0.00)]).

fof(t5_funct_2,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( ( k1_relat_1(C) = A
          & ! [D] : 
              ( r2_hidden(D,A)
             => r2_hidden(k1_funct_1(C,D),B) ) )
       => ( v1_funct_1(C)
          & v1_funct_2(C,A,B)
          & m2_relset_1(C,A,B) ) ) ) ),
    file(funct_2,t5_funct_2),
    [interesting(0.00)]).

fof(t11_realset1,theorem,(
    ! [A] : 
      ( ~ v1_realset1(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m3_realset1(C,A,B)
             => ( v1_funct_1(k1_realset1(C,k4_xboole_0(A,k1_tarski(B))))
                & v1_funct_2(k1_realset1(C,k4_xboole_0(A,k1_tarski(B))),k2_zfmisc_1(k4_xboole_0(A,k1_tarski(B)),k4_xboole_0(A,k1_tarski(B))),k4_xboole_0(A,k1_tarski(B)))
                & m2_relset_1(k1_realset1(C,k4_xboole_0(A,k1_tarski(B))),k2_zfmisc_1(k4_xboole_0(A,k1_tarski(B)),k4_xboole_0(A,k1_tarski(B))),k4_xboole_0(A,k1_tarski(B))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_funct_2,t12_relset_1,t36_xboole_1,t119_zfmisc_1,t91_relat_1,t70_funct_1,d8_realset1,t5_funct_2]),
    [file(realset1,t11_realset1),interesting(0.00)]).

fof(d10_realset1,definition,(
    ! [A] : 
      ( ~ v1_realset1(A)
     => ! [B] : 
          ( m4_realset1(B,A)
        <=> ? [C] : 
              ( m1_subset_1(C,A)
              & B = k1_tarski(C) ) ) ) ),
    file(realset1,d10_realset1),
    [interesting(0.00)]).

fof(t41_zfmisc_1,theorem,(
    ! [A,B] : ~ ( A != k1_tarski(B)
      & A != k1_xboole_0
      & ! [C] : ~ ( r2_hidden(C,A)
          & C != B ) ) ),
    file(zfmisc_1,t41_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(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(d4_realset1,definition,(
    ! [A] : 
      ( v1_realset1(A)
    <=> ~ ( ~ v1_xboole_0(A)
          & ! [B] : A != k1_tarski(B) ) ) ),
    file(realset1,d4_realset1),
    [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(t78_card_1,theorem,(
    k4_card_1(k1_xboole_0) = 0 ),
    file(card_1,t78_card_1),
    [interesting(0.00)]).

fof(t79_card_1,theorem,(
    ! [A] : k4_card_1(k1_tarski(A)) = 1 ),
    file(card_1,t79_card_1),
    [interesting(0.00)]).

fof(t59_card_2,theorem,(
    ! [A] : 
      ( k1_card_1(A) = 0
     => A = k1_xboole_0 ) ),
    file(card_2,t59_card_2),
    [interesting(0.00)]).

fof(t60_card_2,theorem,(
    ! [A] : 
      ( k1_card_1(A) = 1
    <=> ? [B] : A = k1_tarski(B) ) ),
    file(card_2,t60_card_2),
    [interesting(0.00)]).

fof(t71_nat_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( ~ r1_xreal_0(2,A)
          & A != 0
          & A != 1 ) ) ),
    file(nat_1,t71_nat_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(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(t26_zfmisc_1,theorem,(
    ! [A,B,C] : 
      ( r1_tarski(k2_tarski(A,B),k1_tarski(C))
     => A = C ) ),
    file(zfmisc_1,t26_zfmisc_1),
    [interesting(0.00)]).

fof(t113_zfmisc_1,theorem,(
    ! [A,B] : 
      ( k2_zfmisc_1(A,B) = k1_xboole_0
    <=> ( A = k1_xboole_0
        | B = k1_xboole_0 ) ) ),
    file(zfmisc_1,t113_zfmisc_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(d2_realset1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k2_zfmisc_1(A,A),A)
        & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
     => ! [C] : 
          ( m1_subset_1(C,k1_zfmisc_1(A))
         => ( m1_realset1(C,A,B)
          <=> ! [D] : 
                ( r2_hidden(D,k2_zfmisc_1(C,C))
               => r2_hidden(k1_funct_1(B,D),C) ) ) ) ) ),
    file(realset1,d2_realset1),
    [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(d6_realset1,definition,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( ( v1_funct_1(C)
            & v1_funct_2(C,k2_zfmisc_1(A,A),A)
            & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
         => ( m2_realset1(C,A,B)
          <=> ! [D] : 
                ( r2_hidden(D,k2_zfmisc_1(B,B))
               => r2_hidden(k1_funct_1(C,D),B) ) ) ) ) ),
    file(realset1,d6_realset1),
    [interesting(0.00)]).