fof(t24_relat_2,theorem,(
    ! [A] : 
      ( v4_relat_2(k6_relat_1(A))
      & v1_relat_2(k6_relat_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[d4_relat_2,d12_relat_2,d10_relat_1,t23_relat_2,t22_relat_2]),
    [file(relat_2,t24_relat_2),interesting(1.00)]).

fof(t34_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_relat_2(A)
       => v3_relat_2(k4_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_relat_2]),
    [file(relat_2,t34_relat_2),interesting(0.84)]).

fof(t22_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( ( v3_relat_2(A)
          & v8_relat_2(A) )
       => v1_relat_2(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_relat_2,d16_relat_2,d6_relat_1,d4_relat_1,t30_relat_1,d3_relat_2,d8_relat_2,d5_relat_1,t30_relat_1,d3_relat_2,d8_relat_2,d2_xboole_0,d1_relat_2,d9_relat_2]),
    [file(relat_2,t22_relat_2),interesting(0.81)]).

fof(t30_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_relat_2(A)
      <=> A = k4_relat_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_relat_2,t30_relat_1,d3_relat_2,d7_relat_1,d7_relat_1,t30_relat_1,d3_relat_2,d2_relat_1,d7_relat_1,d3_relat_2,d11_relat_2]),
    [file(relat_2,t30_relat_2),interesting(0.79)]).

fof(t44_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v8_relat_2(A)
      <=> r1_tarski(k5_relat_1(A,A),A) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_relat_2,d8_relat_1,t30_relat_1,d8_relat_2,d3_relat_1,d8_relat_1,d8_relat_2,d16_relat_2]),
    [file(relat_2,t44_relat_2),interesting(0.74)]).

fof(t23_relat_2,theorem,(
    ! [A] : 
      ( v3_relat_2(k6_relat_1(A))
      & v8_relat_2(k6_relat_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[d3_relat_2,d11_relat_2,d10_relat_1,d8_relat_2,d16_relat_2,d10_relat_1]),
    [file(relat_2,t23_relat_2),interesting(0.73)]).

fof(t27_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v1_relat_2(A)
       => v1_relat_2(k4_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_relat_2,t38_relat_1,d1_relat_2,d7_relat_1,d1_relat_2,d9_relat_2]),
    [file(relat_2,t27_relat_2),interesting(0.71)]).

fof(t25_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( ( v2_relat_2(A)
          & v8_relat_2(A) )
       => v5_relat_2(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_relat_2,d16_relat_2,d2_relat_2,d8_relat_2,d5_relat_2,d13_relat_2]),
    [file(relat_2,t25_relat_2),interesting(0.68)]).

fof(t42_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v8_relat_2(A)
       => v8_relat_2(k4_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_relat_2,t38_relat_1,d7_relat_1,d8_relat_2,d7_relat_1,d8_relat_2,d16_relat_2]),
    [file(relat_2,t42_relat_2),interesting(0.67)]).

fof(t40_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v4_relat_2(A)
       => v4_relat_2(k4_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_relat_2,t38_relat_1,d7_relat_1,d4_relat_2,d4_relat_2,d12_relat_2]),
    [file(relat_2,t40_relat_2),interesting(0.66)]).

fof(t36_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v5_relat_2(A)
       => v5_relat_2(k4_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d13_relat_2,t38_relat_1,d7_relat_1,d5_relat_2,d7_relat_1,d5_relat_2,d13_relat_2]),
    [file(relat_2,t36_relat_2),interesting(0.65)]).

fof(t26_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v5_relat_2(A)
       => ( v2_relat_2(A)
          & v4_relat_2(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d13_relat_2,d5_relat_2,d2_relat_2,d10_relat_2,d5_relat_2,d4_relat_2,d12_relat_2]),
    [file(relat_2,t26_relat_2),interesting(0.64)]).

fof(t46_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v7_relat_2(A)
       => ( v6_relat_2(A)
          & v1_relat_2(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_relat_2,d7_relat_2,d6_relat_2,d14_relat_2,d1_relat_2,d9_relat_2,d7_relat_2]),
    [file(relat_2,t46_relat_2),interesting(0.64)]).

fof(t28_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v2_relat_2(A)
       => v2_relat_2(k4_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_relat_2,t38_relat_1,d2_relat_2,d7_relat_1,d2_relat_2,d10_relat_2]),
    [file(relat_2,t28_relat_2),interesting(0.63)]).

fof(t33_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( v2_relat_2(A)
           => v2_relat_2(k4_xboole_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_relat_2,d6_relat_1,d4_relat_1,d4_xboole_0,t30_relat_1,d2_relat_2,d5_relat_1,d4_xboole_0,t30_relat_1,d2_relat_2,d2_xboole_0,d4_xboole_0,d2_relat_2,d10_relat_2]),
    [file(relat_2,t33_relat_2),interesting(0.62)]).

fof(t19_relat_2,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r4_relat_2(B,A)
      <=> r5_relat_2(k4_xboole_0(B,k6_relat_1(A)),A) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_xboole_0,d10_relat_1,d4_relat_2,d4_xboole_0,d5_relat_2,d10_relat_1,d4_xboole_0,d5_relat_2,d4_relat_2]),
    [file(relat_2,t19_relat_2),interesting(0.58)]).

fof(t20_relat_2,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r5_relat_2(B,A)
       => r4_relat_2(k2_xboole_0(B,k6_relat_1(A)),A) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_relat_1,d2_xboole_0,d5_relat_2,d4_relat_2]),
    [file(relat_2,t20_relat_2),interesting(0.58)]).

fof(t38_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( v5_relat_2(A)
           => v5_relat_2(k4_xboole_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d13_relat_2,d4_xboole_0,t30_relat_1,d5_relat_2,d4_xboole_0,d5_relat_2,d13_relat_2]),
    [file(relat_2,t38_relat_2),interesting(0.58)]).

fof(t18_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v2_relat_2(A)
      <=> r1_xboole_0(k6_relat_1(k3_relat_1(A)),A) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_relat_2,d3_xboole_0,d10_relat_1,d2_relat_2,t56_relat_1,d7_xboole_0,d10_relat_1,t3_xboole_0,d2_relat_2,d10_relat_2]),
    [file(relat_2,t18_relat_2),interesting(0.56)]).

fof(t43_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( ( v8_relat_2(A)
              & v8_relat_2(B) )
           => v8_relat_2(k3_xboole_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_relat_2,d16_relat_2,d3_xboole_0,t30_relat_1,d8_relat_2,d3_xboole_0,d8_relat_2,d16_relat_2]),
    [file(relat_2,t43_relat_2),interesting(0.54)]).

fof(t17_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v1_relat_2(A)
      <=> r1_tarski(k6_relat_1(k3_relat_1(A)),A) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_relat_2,d10_relat_1,d1_relat_2,d3_relat_1,d10_relat_1,d1_relat_2,d9_relat_2]),
    [file(relat_2,t17_relat_2),interesting(0.51)]).

fof(t37_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( ( v5_relat_2(A)
              & v5_relat_2(B) )
           => v5_relat_2(k3_xboole_0(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d13_relat_2,t34_relat_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d5_relat_2,d3_xboole_0,d5_relat_2,d13_relat_2]),
    [file(relat_2,t37_relat_2),interesting(0.51)]).

fof(t41_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( v4_relat_2(A)
           => ( v4_relat_2(k3_xboole_0(A,B))
              & v4_relat_2(k4_xboole_0(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_relat_2,d3_xboole_0,t30_relat_1,d4_relat_2,d4_relat_2,d12_relat_2,d4_xboole_0,t30_relat_1,d4_relat_2,d4_relat_2,d12_relat_2]),
    [file(relat_2,t41_relat_2),interesting(0.45)]).

fof(t32_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( ( v2_relat_2(A)
              & v2_relat_2(B) )
           => ( v2_relat_2(k2_xboole_0(A,B))
              & v2_relat_2(k3_xboole_0(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_relat_2,d10_relat_2,t33_relat_1,d2_relat_2,d2_relat_2,t30_relat_1,d2_xboole_0,d2_relat_2,d2_relat_2,t30_relat_1,d2_xboole_0,d2_xboole_0,d2_relat_2,d10_relat_2,t34_relat_1,d3_xboole_0,d2_relat_2,d3_xboole_0,d2_relat_2,d10_relat_2]),
    [file(relat_2,t32_relat_2),interesting(0.43)]).

fof(t31_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( ( v1_relat_2(A)
              & v1_relat_2(B) )
           => ( v1_relat_2(k2_xboole_0(A,B))
              & v1_relat_2(k3_xboole_0(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_relat_2,d9_relat_2,t33_relat_1,d1_relat_2,d2_xboole_0,d1_relat_2,d2_xboole_0,d2_xboole_0,d1_relat_2,d9_relat_2,t34_relat_1,d3_xboole_0,d1_relat_2,d3_xboole_0,d1_relat_2,d9_relat_2]),
    [file(relat_2,t31_relat_2),interesting(0.41)]).

fof(t39_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v4_relat_2(A)
      <=> r1_tarski(k3_xboole_0(A,k4_relat_1(A)),k6_relat_1(k1_relat_1(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_relat_2,d3_xboole_0,t30_relat_1,d7_relat_1,d4_relat_2,d4_relat_1,d10_relat_1,d3_relat_1,d7_relat_1,d3_xboole_0,d10_relat_1,d4_relat_2,d12_relat_2]),
    [file(relat_2,t39_relat_2),interesting(0.41)]).

fof(t29_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v1_relat_2(A)
       => ( k1_relat_1(A) = k1_relat_1(k4_relat_1(A))
          & k2_relat_1(A) = k2_relat_1(k4_relat_1(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_relat_2,t27_relat_2,d9_relat_2,d2_xboole_0,d6_relat_1,d1_relat_2,d7_relat_1,d4_relat_1,d2_xboole_0,d6_relat_1,d1_relat_2,d7_relat_1,d4_relat_1,t2_tarski,d2_xboole_0,d6_relat_1,d1_relat_2,d7_relat_1,d5_relat_1,d2_xboole_0,d6_relat_1,d1_relat_2,d7_relat_1,d5_relat_1,t2_tarski]),
    [file(relat_2,t29_relat_2),interesting(0.38)]).

fof(t47_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v7_relat_2(A)
      <=> k2_zfmisc_1(k3_relat_1(A),k3_relat_1(A)) = k2_xboole_0(A,k4_relat_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_relat_2,d2_zfmisc_1,d7_relat_2,d7_relat_1,d2_xboole_0,d1_relat_1,d2_xboole_0,d7_relat_1,t30_relat_1,t106_zfmisc_1,t2_tarski,t106_zfmisc_1,d2_xboole_0,d7_relat_1,d7_relat_2,d15_relat_2]),
    [file(relat_2,t47_relat_2),interesting(0.38)]).

fof(t35_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( ( v3_relat_2(A)
              & v3_relat_2(B) )
           => ( v3_relat_2(k2_xboole_0(A,B))
              & v3_relat_2(k3_xboole_0(A,B))
              & v3_relat_2(k4_xboole_0(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_relat_2,d11_relat_2,t30_relat_1,d3_relat_2,d2_xboole_0,t30_relat_1,d3_relat_2,d2_xboole_0,d2_xboole_0,d3_relat_2,d11_relat_2,t34_relat_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_relat_2,d3_relat_2,d3_xboole_0,d3_relat_2,d11_relat_2,d4_xboole_0,t30_relat_1,d3_relat_2,d3_relat_2,t30_relat_1,d4_xboole_0,d3_relat_2,d11_relat_2]),
    [file(relat_2,t35_relat_2),interesting(0.28)]).

fof(t10_relat_2,theorem,(
    $true ),
    file(relat_2,t10_relat_2),
    [interesting(0.00)]).

fof(t11_relat_2,theorem,(
    $true ),
    file(relat_2,t11_relat_2),
    [interesting(0.00)]).

fof(t12_relat_2,theorem,(
    $true ),
    file(relat_2,t12_relat_2),
    [interesting(0.00)]).

fof(t13_relat_2,theorem,(
    $true ),
    file(relat_2,t13_relat_2),
    [interesting(0.00)]).

fof(t14_relat_2,theorem,(
    $true ),
    file(relat_2,t14_relat_2),
    [interesting(0.00)]).

fof(t15_relat_2,theorem,(
    $true ),
    file(relat_2,t15_relat_2),
    [interesting(0.00)]).

fof(t16_relat_2,theorem,(
    $true ),
    file(relat_2,t16_relat_2),
    [interesting(0.00)]).

fof(d9_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v1_relat_2(A)
      <=> r1_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d9_relat_2),
    [interesting(0.00)]).

fof(d10_relat_1,definition,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( B = k6_relat_1(A)
      <=> ! [C,D] : 
            ( r2_hidden(k4_tarski(C,D),B)
          <=> ( r2_hidden(C,A)
              & C = D ) ) ) ) ),
    file(relat_1,d10_relat_1),
    [interesting(0.00)]).

fof(d1_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r1_relat_2(A,B)
        <=> ! [C] : 
              ( r2_hidden(C,B)
             => r2_hidden(k4_tarski(C,C),A) ) ) ) ),
    file(relat_2,d1_relat_2),
    [interesting(0.00)]).

fof(d3_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( r1_tarski(A,B)
          <=> ! [C,D] : 
                ( r2_hidden(k4_tarski(C,D),A)
               => r2_hidden(k4_tarski(C,D),B) ) ) ) ) ),
    file(relat_1,d3_relat_1),
    [interesting(0.00)]).

fof(d10_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v2_relat_2(A)
      <=> r2_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d10_relat_2),
    [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_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r2_relat_2(A,B)
        <=> ! [C] : ~ ( r2_hidden(C,B)
              & r2_hidden(k4_tarski(C,C),A) ) ) ) ),
    file(relat_2,d2_relat_2),
    [interesting(0.00)]).

fof(t56_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( ! [B,C] : ~ r2_hidden(k4_tarski(B,C),A)
       => A = k1_xboole_0 ) ) ),
    file(relat_1,t56_relat_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(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(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_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r4_relat_2(A,B)
        <=> ! [C,D] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(k4_tarski(C,D),A)
                & r2_hidden(k4_tarski(D,C),A) )
             => C = D ) ) ) ),
    file(relat_2,d4_relat_2),
    [interesting(0.00)]).

fof(d5_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r5_relat_2(A,B)
        <=> ! [C,D] : ~ ( r2_hidden(C,B)
              & r2_hidden(D,B)
              & r2_hidden(k4_tarski(C,D),A)
              & r2_hidden(k4_tarski(D,C),A) ) ) ) ),
    file(relat_2,d5_relat_2),
    [interesting(0.00)]).

fof(t1_relat_2,theorem,(
    $true ),
    file(relat_2,t1_relat_2),
    [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(t21_relat_2,theorem,(
    $true ),
    file(relat_2,t21_relat_2),
    [interesting(0.00)]).

fof(d12_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v4_relat_2(A)
      <=> r4_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d12_relat_2),
    [interesting(0.00)]).

fof(d3_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r3_relat_2(A,B)
        <=> ! [C,D] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(k4_tarski(C,D),A) )
             => r2_hidden(k4_tarski(D,C),A) ) ) ) ),
    file(relat_2,d3_relat_2),
    [interesting(0.00)]).

fof(d11_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v3_relat_2(A)
      <=> r3_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d11_relat_2),
    [interesting(0.00)]).

fof(d8_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r8_relat_2(A,B)
        <=> ! [C,D,E] : 
              ( ( r2_hidden(C,B)
                & r2_hidden(D,B)
                & r2_hidden(E,B)
                & r2_hidden(k4_tarski(C,D),A)
                & r2_hidden(k4_tarski(D,E),A) )
             => r2_hidden(k4_tarski(C,E),A) ) ) ) ),
    file(relat_2,d8_relat_2),
    [interesting(0.00)]).

fof(d16_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v8_relat_2(A)
      <=> r8_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d16_relat_2),
    [interesting(0.00)]).

fof(d6_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => k3_relat_1(A) = k2_xboole_0(k1_relat_1(A),k2_relat_1(A)) ) ),
    file(relat_1,d6_relat_1),
    [interesting(0.00)]).

fof(d4_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( B = k1_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : r2_hidden(k4_tarski(C,D),A) ) ) ) ),
    file(relat_1,d4_relat_1),
    [interesting(0.00)]).

fof(t30_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( r2_hidden(k4_tarski(A,B),C)
       => ( r2_hidden(A,k3_relat_1(C))
          & r2_hidden(B,k3_relat_1(C)) ) ) ) ),
    file(relat_1,t30_relat_1),
    [interesting(0.00)]).

fof(d5_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( B = k2_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : r2_hidden(k4_tarski(D,C),A) ) ) ) ),
    file(relat_1,d5_relat_1),
    [interesting(0.00)]).

fof(d13_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v5_relat_2(A)
      <=> r5_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d13_relat_2),
    [interesting(0.00)]).

fof(t38_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => k3_relat_1(A) = k3_relat_1(k4_relat_1(A)) ) ),
    file(relat_1,t38_relat_1),
    [interesting(0.00)]).

fof(d7_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( B = k4_relat_1(A)
          <=> ! [C,D] : 
                ( r2_hidden(k4_tarski(C,D),B)
              <=> r2_hidden(k4_tarski(D,C),A) ) ) ) ) ),
    file(relat_1,d7_relat_1),
    [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(t2_relat_2,theorem,(
    $true ),
    file(relat_2,t2_relat_2),
    [interesting(0.00)]).

fof(t33_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => k3_relat_1(k2_xboole_0(A,B)) = k2_xboole_0(k3_relat_1(A),k3_relat_1(B)) ) ) ),
    file(relat_1,t33_relat_1),
    [interesting(0.00)]).

fof(t34_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => r1_tarski(k3_relat_1(k3_xboole_0(A,B)),k3_xboole_0(k3_relat_1(A),k3_relat_1(B))) ) ) ),
    file(relat_1,t34_relat_1),
    [interesting(0.00)]).

fof(d2_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ( A = B
          <=> ! [C,D] : 
                ( r2_hidden(k4_tarski(C,D),A)
              <=> r2_hidden(k4_tarski(C,D),B) ) ) ) ) ),
    file(relat_1,d2_relat_1),
    [interesting(0.00)]).

fof(t3_relat_2,theorem,(
    $true ),
    file(relat_2,t3_relat_2),
    [interesting(0.00)]).

fof(d8_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ! [C] : 
              ( v1_relat_1(C)
             => ( C = k5_relat_1(A,B)
              <=> ! [D,E] : 
                    ( r2_hidden(k4_tarski(D,E),C)
                  <=> ? [F] : 
                        ( r2_hidden(k4_tarski(D,F),A)
                        & r2_hidden(k4_tarski(F,E),B) ) ) ) ) ) ) ),
    file(relat_1,d8_relat_1),
    [interesting(0.00)]).

fof(d14_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v6_relat_2(A)
      <=> r6_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d14_relat_2),
    [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(d6_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r6_relat_2(A,B)
        <=> ! [C,D] : ~ ( r2_hidden(C,B)
              & r2_hidden(D,B)
              & C != D
              & ~ r2_hidden(k4_tarski(C,D),A)
              & ~ r2_hidden(k4_tarski(D,C),A) ) ) ) ),
    file(relat_2,d6_relat_2),
    [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(t45_relat_2,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v6_relat_2(A)
      <=> r1_tarski(k4_xboole_0(k2_zfmisc_1(k3_relat_1(A),k3_relat_1(A)),k6_relat_1(k3_relat_1(A))),k2_xboole_0(A,k4_relat_1(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[d14_relat_2,d4_xboole_0,d2_zfmisc_1,d10_relat_1,d6_relat_2,d7_relat_1,d2_xboole_0,d3_tarski,d4_xboole_0,d10_relat_1,d2_xboole_0,t106_zfmisc_1,d7_relat_1,d6_relat_2,d14_relat_2]),
    [file(relat_2,t45_relat_2),interesting(0.00)]).

fof(d15_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( v7_relat_2(A)
      <=> r7_relat_2(A,k3_relat_1(A)) ) ) ),
    file(relat_2,d15_relat_2),
    [interesting(0.00)]).

fof(d7_relat_2,definition,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( r7_relat_2(A,B)
        <=> ! [C,D] : ~ ( r2_hidden(C,B)
              & r2_hidden(D,B)
              & ~ r2_hidden(k4_tarski(C,D),A)
              & ~ r2_hidden(k4_tarski(D,C),A) ) ) ) ),
    file(relat_2,d7_relat_2),
    [interesting(0.00)]).

fof(d1_relat_1,definition,(
    ! [A] : 
      ( v1_relat_1(A)
    <=> ! [B] : ~ ( r2_hidden(B,A)
          & ! [C,D] : B != k4_tarski(C,D) ) ) ),
    file(relat_1,d1_relat_1),
    [interesting(0.00)]).

fof(t4_relat_2,theorem,(
    $true ),
    file(relat_2,t4_relat_2),
    [interesting(0.00)]).

fof(t5_relat_2,theorem,(
    $true ),
    file(relat_2,t5_relat_2),
    [interesting(0.00)]).

fof(t6_relat_2,theorem,(
    $true ),
    file(relat_2,t6_relat_2),
    [interesting(0.00)]).

fof(t7_relat_2,theorem,(
    $true ),
    file(relat_2,t7_relat_2),
    [interesting(0.00)]).

fof(t8_relat_2,theorem,(
    $true ),
    file(relat_2,t8_relat_2),
    [interesting(0.00)]).

fof(t9_relat_2,theorem,(
    $true ),
    file(relat_2,t9_relat_2),
    [interesting(0.00)]).