fof(t30_axioms,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => A = a_1_0_axioms(A) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d21_ordinal2,d2_ordinal1,t2_arytm_2,t2_arytm_2,t19_arytm_2,d2_xreal_0,l21_axioms,d10_xboole_0,d3_tarski,d21_ordinal2,t2_arytm_2,d2_xreal_0,t19_arytm_2]),
    [file(axioms,t30_axioms),interesting(1.00)]).

fof(t28_axioms,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r2_hidden(A,k5_numbers)
              & r2_hidden(B,k5_numbers) )
           => r2_hidden(k2_xcmplx_0(A,B),k5_numbers) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_xreal_0,l23_axioms,d2_arytm_0,t2_arytm_2,t17_arytm_2]),
    [file(axioms,t28_axioms),interesting(0.64)]).

fof(l34_axioms,theorem,(
    k4_ordinal2 = 1 ),
    inference(mizar_proof,[status(thm)],[d4_ordinal2]),
    [file(axioms,l34_axioms),interesting(0.54)]).

fof(l24_axioms,theorem,(
    r2_hidden(k1_xboole_0,k1_tarski(k1_xboole_0)) ),
    inference(mizar_proof,[status(thm)],[d1_tarski]),
    [file(axioms,l24_axioms),interesting(0.51)]).

fof(l21_axioms,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(A,B)
              & r1_xreal_0(B,A) )
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_xreal_1]),
    [file(axioms,l21_axioms),interesting(0.49)]).

fof(l25_axioms,theorem,(
    m1_subset_1(0,k2_arytm_2) ),
    inference(mizar_proof,[status(thm)],[t21_arytm_2]),
    [file(axioms,l25_axioms),interesting(0.43)]).

fof(l23_axioms,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ( ( A = C
                      & B = D )
                   => k1_arytm_0(A,B) = k2_xcmplx_0(C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_xcmplx_0,l22_axioms,l22_axioms,t13_arytm_0,d7_arytm_0]),
    [file(axioms,l23_axioms),interesting(0.32)]).

fof(l22_axioms,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ( A = k5_arytm_0(B,C)
               => ( C = 0
                  & A = B ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_xreal_0,d7_arytm_0,t10_arytm_0,d7_arytm_0]),
    [file(axioms,l22_axioms),interesting(0.12)]).

fof(t20_axioms,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ ( A != 0
          & ! [B] : 
              ( v1_xreal_0(B)
             => k3_xcmplx_0(A,B) != 1 ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_xcmplx_0]),
    [file(axioms,t20_axioms),interesting(0.07)]).

fof(t29_axioms,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(k1_numbers))
     => ( ( r2_hidden(0,A)
          & ! [B] : 
              ( v1_xreal_0(B)
             => ( r2_hidden(B,A)
               => r2_hidden(k2_xcmplx_0(B,1),A) ) ) )
       => r1_tarski(k5_numbers,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t17_xboole_1,t21_arytm_2,d3_xboole_0,t17_xboole_1,t1_arytm_0,d1_xreal_0,l34_axioms,d2_arytm_0,t21_arytm_2,l23_axioms,d3_xboole_0,l34_axioms,t18_arytm_2,t1_xboole_1]),
    [file(axioms,t29_axioms),interesting(0.05)]).

fof(t21_arytm_2,theorem,
    ( r2_hidden(k12_arytm_3,k2_arytm_2)
    & r2_hidden(k13_arytm_3,k2_arytm_2) ),
    file(arytm_2,t21_arytm_2),
    [interesting(0.00)]).

fof(t10_axioms,theorem,(
    $true ),
    file(axioms,t10_axioms),
    [interesting(0.00)]).

fof(t11_axioms,theorem,(
    $true ),
    file(axioms,t11_axioms),
    [interesting(0.00)]).

fof(t12_axioms,theorem,(
    $true ),
    file(axioms,t12_axioms),
    [interesting(0.00)]).

fof(t13_axioms,theorem,(
    $true ),
    file(axioms,t13_axioms),
    [interesting(0.00)]).

fof(t14_axioms,theorem,(
    $true ),
    file(axioms,t14_axioms),
    [interesting(0.00)]).

fof(t15_axioms,theorem,(
    $true ),
    file(axioms,t15_axioms),
    [interesting(0.00)]).

fof(t16_axioms,theorem,(
    $true ),
    file(axioms,t16_axioms),
    [interesting(0.00)]).

fof(t17_axioms,theorem,(
    $true ),
    file(axioms,t17_axioms),
    [interesting(0.00)]).

fof(t18_axioms,theorem,(
    $true ),
    file(axioms,t18_axioms),
    [interesting(0.00)]).

fof(t19_axioms,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ? [B] : 
          ( v1_xreal_0(B)
          & k2_xcmplx_0(A,B) = 0 ) ) ),
    file(axioms,t19_axioms),
    [interesting(0.00)]).

fof(t1_axioms,theorem,(
    $true ),
    file(axioms,t1_axioms),
    [interesting(0.00)]).

fof(d7_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( A != 0
             => ( B = k5_xcmplx_0(A)
              <=> k3_xcmplx_0(A,B) = 1 ) )
            & ( A = 0
             => ( B = k5_xcmplx_0(A)
              <=> B = 0 ) ) ) ) ) ),
    file(xcmplx_0,d7_xcmplx_0),
    [interesting(0.00)]).

fof(t21_axioms,theorem,(
    $true ),
    file(axioms,t21_axioms),
    [interesting(0.00)]).

fof(t22_axioms,theorem,(
    $true ),
    file(axioms,t22_axioms),
    [interesting(0.00)]).

fof(t23_axioms,theorem,(
    $true ),
    file(axioms,t23_axioms),
    [interesting(0.00)]).

fof(t24_axioms,theorem,(
    $true ),
    file(axioms,t24_axioms),
    [interesting(0.00)]).

fof(t25_axioms,theorem,(
    $true ),
    file(axioms,t25_axioms),
    [interesting(0.00)]).

fof(t10_subset_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ~ ( B != k1_xboole_0
          & ! [C] : 
              ( m1_subset_1(C,A)
             => ~ r2_hidden(C,B) ) ) ) ),
    file(subset_1,t10_subset_1),
    [interesting(0.00)]).

fof(d1_numbers,definition,(
    k1_numbers = k4_xboole_0(k2_xboole_0(k2_arytm_2,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)),k1_tarski(k4_tarski(0,0))) ),
    file(numbers,d1_numbers),
    [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(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(t73_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,k2_xboole_0(B,C))
        & r1_xboole_0(A,C) )
     => r1_tarski(A,B) ) ),
    file(xboole_1,t73_xboole_1),
    [interesting(0.00)]).

fof(t5_arytm_0,theorem,(
    r1_subset_1(k2_arytm_2,k2_zfmisc_1(k1_tarski(k12_arytm_3),k2_arytm_2)) ),
    file(arytm_0,t5_arytm_0),
    [interesting(0.00)]).

fof(t3_xboole_0,theorem,(
    ! [A,B] : 
      ( ~ ( ~ r1_xboole_0(A,B)
          & ! [C] : ~ ( r2_hidden(C,A)
              & r2_hidden(C,B) ) )
      & ~ ( ? [C] : 
              ( r2_hidden(C,A)
              & r2_hidden(C,B) )
          & r1_xboole_0(A,B) ) ) ),
    file(xboole_0,t3_xboole_0),
    [interesting(0.00)]).

fof(d2_xreal_0,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( ( r2_hidden(A,k2_arytm_2)
                & r2_hidden(B,k2_arytm_2) )
             => ( r1_xreal_0(A,B)
              <=> ? [C] : 
                    ( m1_subset_1(C,k2_arytm_2)
                    & ? [D] : 
                        ( m1_subset_1(D,k2_arytm_2)
                        & A = C
                        & B = D
                        & r1_arytm_2(C,D) ) ) ) )
            & ( ( r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2))
                & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) )
             => ( r1_xreal_0(A,B)
              <=> ? [C] : 
                    ( m1_subset_1(C,k2_arytm_2)
                    & ? [D] : 
                        ( m1_subset_1(D,k2_arytm_2)
                        & A = k4_tarski(0,C)
                        & B = k4_tarski(0,D)
                        & r1_arytm_2(D,C) ) ) ) )
            & ~ ( ~ ( r2_hidden(A,k2_arytm_2)
                    & r2_hidden(B,k2_arytm_2) )
                & ~ ( r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2))
                    & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) )
                & ~ ( r1_xreal_0(A,B)
                  <=> ( r2_hidden(B,k2_arytm_2)
                      & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) ) ) ) ) ) ),
    file(xreal_0,d2_xreal_0),
    [interesting(0.00)]).

fof(t6_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( A = k1_xboole_0
           => r1_arytm_2(A,B) ) ) ) ),
    file(arytm_1,t6_arytm_1),
    [interesting(0.00)]).

fof(t103_zfmisc_1,theorem,(
    ! [A,B,C,D] : ~ ( r1_tarski(A,k2_zfmisc_1(B,C))
      & r2_hidden(D,A)
      & ! [E,F] : ~ ( r2_hidden(E,B)
          & r2_hidden(F,C)
          & D = k4_tarski(E,F) ) ) ),
    file(zfmisc_1,t103_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(d1_xreal_0,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
    <=> r2_hidden(A,k1_numbers) ) ),
    file(xreal_0,d1_xreal_0),
    [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(t106_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))
    <=> ( r2_hidden(A,C)
        & r2_hidden(B,D) ) ) ),
    file(zfmisc_1,t106_zfmisc_1),
    [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(t33_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( k4_tarski(A,B) = k4_tarski(C,D)
     => ( A = C
        & B = D ) ) ),
    file(zfmisc_1,t33_zfmisc_1),
    [interesting(0.00)]).

fof(t9_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(k2_arytm_2))
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k2_arytm_2))
         => ~ ( ? [C] : 
                  ( m1_subset_1(C,k2_arytm_2)
                  & r2_hidden(C,A) )
              & ? [C] : 
                  ( m1_subset_1(C,k2_arytm_2)
                  & r2_hidden(C,B) )
              & ! [C] : 
                  ( m1_subset_1(C,k2_arytm_2)
                 => ! [D] : 
                      ( m1_subset_1(D,k2_arytm_2)
                     => ( ( r2_hidden(C,A)
                          & r2_hidden(D,B) )
                       => r1_arytm_2(C,D) ) ) )
              & ! [C] : 
                  ( m1_subset_1(C,k2_arytm_2)
                 => ? [D] : 
                      ( m1_subset_1(D,k2_arytm_2)
                      & ? [E] : 
                          ( m1_subset_1(E,k2_arytm_2)
                          & r2_hidden(D,A)
                          & r2_hidden(E,B)
                          & ~ ( r1_arytm_2(D,C)
                              & r1_arytm_2(C,E) ) ) ) ) ) ) ) ),
    file(arytm_2,t9_arytm_2),
    [interesting(0.00)]).

fof(t3_arytm_0,theorem,(
    ! [A] : ~ ( r2_hidden(k4_tarski(k12_arytm_3,A),k1_numbers)
      & A = k12_arytm_3 ) ),
    file(arytm_0,t3_arytm_0),
    [interesting(0.00)]).

fof(t5_arytm_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( ( r1_arytm_2(A,B)
              & B = k1_xboole_0 )
           => A = k1_xboole_0 ) ) ) ),
    file(arytm_1,t5_arytm_1),
    [interesting(0.00)]).

fof(t2_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ( A != k12_arytm_3
       => r2_hidden(k4_tarski(k12_arytm_3,A),k1_numbers) ) ) ),
    file(arytm_0,t2_arytm_0),
    [interesting(0.00)]).

fof(t1_arytm_0,theorem,(
    r1_tarski(k2_arytm_2,k1_numbers) ),
    file(arytm_0,t1_arytm_0),
    [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(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(t26_axioms,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(k1_numbers))
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(k1_numbers))
         => ~ ( ! [C] : 
                  ( v1_xreal_0(C)
                 => ! [D] : 
                      ( v1_xreal_0(D)
                     => ( ( r2_hidden(C,A)
                          & r2_hidden(D,B) )
                       => r1_xreal_0(C,D) ) ) )
              & ! [C] : 
                  ( v1_xreal_0(C)
                 => ? [D] : 
                      ( v1_xreal_0(D)
                      & ? [E] : 
                          ( v1_xreal_0(E)
                          & r2_hidden(D,A)
                          & r2_hidden(E,B)
                          & ~ ( r1_xreal_0(D,C)
                              & r1_xreal_0(C,E) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_subset_1,t10_subset_1,d1_numbers,t36_xboole_1,t1_xboole_1,t1_xboole_1,t73_xboole_1,t5_arytm_0,t21_arytm_2,t3_xboole_0,d2_xreal_0,t6_arytm_1,d2_xreal_0,t3_xboole_0,t103_zfmisc_1,d1_tarski,d1_xreal_0,d3_tarski,l24_axioms,t106_zfmisc_1,d1_tarski,d3_tarski,d1_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xboole_0,t103_zfmisc_1,d1_tarski,d3_tarski,d1_xreal_0,l24_axioms,t106_zfmisc_1,d2_xreal_0,t33_zfmisc_1,t9_arytm_2,t3_arytm_0,t5_arytm_1,t2_arytm_0,d1_xreal_0,l24_axioms,t106_zfmisc_1,t103_zfmisc_1,d1_tarski,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,t103_zfmisc_1,d1_tarski,d2_xreal_0,d2_xboole_0,t3_xboole_0,t1_arytm_0,d1_xreal_0,t17_xboole_1,d3_xboole_0,d3_tarski,d1_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xboole_0,t1_arytm_0,d1_xreal_0,t17_xboole_1,d2_xreal_0,t9_arytm_2,t1_arytm_0,d1_xreal_0,d3_xboole_0,d2_xreal_0,t5_arytm_0,t3_xboole_0,d2_xreal_0,d2_xreal_0,d2_xboole_0]),
    [file(axioms,t26_axioms),interesting(0.00)]).

fof(t27_axioms,theorem,(
    $true ),
    file(axioms,t27_axioms),
    [interesting(0.00)]).

fof(d4_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( C = k2_xcmplx_0(A,B)
            <=> ? [D] : 
                  ( m1_subset_1(D,k1_numbers)
                  & ? [E] : 
                      ( m1_subset_1(E,k1_numbers)
                      & ? [F] : 
                          ( m1_subset_1(F,k1_numbers)
                          & ? [G] : 
                              ( m1_subset_1(G,k1_numbers)
                              & A = k5_arytm_0(D,E)
                              & B = k5_arytm_0(F,G)
                              & C = k5_arytm_0(k1_arytm_0(D,F),k1_arytm_0(E,G)) ) ) ) ) ) ) ) ),
    file(xcmplx_0,d4_xcmplx_0),
    [interesting(0.00)]).

fof(d7_arytm_0,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( ( B = 0
             => k5_arytm_0(A,B) = A )
            & ( B != 0
             => k5_arytm_0(A,B) = k5_funct_4(k1_numbers,0,k13_arytm_3,A,B) ) ) ) ) ),
    file(arytm_0,d7_arytm_0),
    [interesting(0.00)]).

fof(t10_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ~ r2_hidden(k5_funct_4(k1_numbers,0,k13_arytm_3,A,B),k1_numbers) ) ) ),
    file(arytm_0,t10_arytm_0),
    [interesting(0.00)]).

fof(t13_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = 0
           => k1_arytm_0(A,B) = A ) ) ) ),
    file(arytm_0,t13_arytm_0),
    [interesting(0.00)]).

fof(d2_arytm_0,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ( ( ( r2_hidden(A,k2_arytm_2)
                    & r2_hidden(B,k2_arytm_2) )
                 => ( C = k1_arytm_0(A,B)
                  <=> ? [D] : 
                        ( m1_subset_1(D,k2_arytm_2)
                        & ? [E] : 
                            ( m1_subset_1(E,k2_arytm_2)
                            & A = D
                            & B = E
                            & C = k7_arytm_2(D,E) ) ) ) )
                & ( ( r2_hidden(A,k2_arytm_2)
                    & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) )
                 => ( C = k1_arytm_0(A,B)
                  <=> ? [D] : 
                        ( m1_subset_1(D,k2_arytm_2)
                        & ? [E] : 
                            ( m1_subset_1(E,k2_arytm_2)
                            & A = D
                            & B = k4_tarski(0,E)
                            & C = k2_arytm_1(D,E) ) ) ) )
                & ( ( r2_hidden(B,k2_arytm_2)
                    & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) )
                 => ( C = k1_arytm_0(A,B)
                  <=> ? [D] : 
                        ( m1_subset_1(D,k2_arytm_2)
                        & ? [E] : 
                            ( m1_subset_1(E,k2_arytm_2)
                            & A = k4_tarski(0,D)
                            & B = E
                            & C = k2_arytm_1(E,D) ) ) ) )
                & ~ ( ~ ( r2_hidden(A,k2_arytm_2)
                        & r2_hidden(B,k2_arytm_2) )
                    & ~ ( r2_hidden(A,k2_arytm_2)
                        & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) )
                    & ~ ( r2_hidden(B,k2_arytm_2)
                        & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) )
                    & ~ ( C = k1_arytm_0(A,B)
                      <=> ? [D] : 
                            ( m1_subset_1(D,k2_arytm_2)
                            & ? [E] : 
                                ( m1_subset_1(E,k2_arytm_2)
                                & A = k4_tarski(0,D)
                                & B = k4_tarski(0,E)
                                & C = k4_tarski(0,k7_arytm_2(D,E)) ) ) ) ) ) ) ) ) ),
    file(arytm_0,d2_arytm_0),
    [interesting(0.00)]).

fof(t2_arytm_2,theorem,(
    r1_tarski(k5_ordinal2,k2_arytm_2) ),
    file(arytm_2,t2_arytm_2),
    [interesting(0.00)]).

fof(t17_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ! [B] : 
          ( m1_subset_1(B,k2_arytm_2)
         => ( ( r2_hidden(A,k5_ordinal2)
              & r2_hidden(B,k5_ordinal2) )
           => r2_hidden(k7_arytm_2(B,A),k5_ordinal2) ) ) ) ),
    file(arytm_2,t17_arytm_2),
    [interesting(0.00)]).

fof(d4_ordinal2,definition,(
    k4_ordinal2 = k1_ordinal1(k1_xboole_0) ),
    file(ordinal2,d4_ordinal2),
    [interesting(0.00)]).

fof(t18_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_zfmisc_1(k2_arytm_2))
     => ( ( r2_hidden(k12_arytm_3,A)
          & ! [B] : 
              ( m1_subset_1(B,k2_arytm_2)
             => ! [C] : 
                  ( m1_subset_1(C,k2_arytm_2)
                 => ( ( r2_hidden(B,A)
                      & C = k13_arytm_3 )
                   => r2_hidden(k7_arytm_2(B,C),A) ) ) ) )
       => r1_tarski(k5_ordinal2,A) ) ) ),
    file(arytm_2,t18_arytm_2),
    [interesting(0.00)]).

fof(t2_axioms,theorem,(
    $true ),
    file(axioms,t2_axioms),
    [interesting(0.00)]).

fof(d21_ordinal2,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
    <=> r2_hidden(A,k5_ordinal2) ) ),
    file(ordinal2,d21_ordinal2),
    [interesting(0.00)]).

fof(d2_ordinal1,definition,(
    ! [A] : 
      ( v1_ordinal1(A)
    <=> ! [B] : 
          ( r2_hidden(B,A)
         => r1_tarski(B,A) ) ) ),
    file(ordinal1,d2_ordinal1),
    [interesting(0.00)]).

fof(t19_arytm_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_arytm_2)
     => ( r2_hidden(A,k5_ordinal2)
       => ! [B] : 
            ( m1_subset_1(B,k2_arytm_2)
           => ( r2_hidden(B,A)
            <=> ( r2_hidden(B,k5_ordinal2)
                & B != A
                & r1_arytm_2(B,A) ) ) ) ) ) ),
    file(arytm_2,t19_arytm_2),
    [interesting(0.00)]).

fof(t1_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(A,B)
              & r1_xreal_0(B,A) )
           => A = B ) ) ) ),
    file(xreal_1,t1_xreal_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(t3_axioms,theorem,(
    $true ),
    file(axioms,t3_axioms),
    [interesting(0.00)]).

fof(t4_axioms,theorem,(
    $true ),
    file(axioms,t4_axioms),
    [interesting(0.00)]).

fof(t5_axioms,theorem,(
    $true ),
    file(axioms,t5_axioms),
    [interesting(0.00)]).

fof(t6_axioms,theorem,(
    $true ),
    file(axioms,t6_axioms),
    [interesting(0.00)]).

fof(t7_axioms,theorem,(
    $true ),
    file(axioms,t7_axioms),
    [interesting(0.00)]).

fof(t8_axioms,theorem,(
    $true ),
    file(axioms,t8_axioms),
    [interesting(0.00)]).

fof(t9_axioms,theorem,(
    $true ),
    file(axioms,t9_axioms),
    [interesting(0.00)]).