fof(t53_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v17_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r3_lattices(A,B,C)
               => r3_lattices(A,k7_lattices(A,C),k7_lattices(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_lattices,t47_lattices,t41_lattices,t26_lattices,t52_lattices]),
    [file(lattices,t53_lattices),interesting(1.00)]).

fof(t41_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v13_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => r3_lattices(A,k5_lattices(A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[t22_lattices,t39_lattices]),
    [file(lattices,t41_lattices),interesting(0.83)]).

fof(t49_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v17_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k7_lattices(A,k7_lattices(A,B)) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d21_lattices,d18_lattices,d21_lattices,d18_lattices,t32_lattices]),
    [file(lattices,t49_lattices),interesting(0.79)]).

fof(t25_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v5_lattices(A)
        & l2_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( ( r1_lattices(A,B,C)
                      & r1_lattices(A,C,D) )
                   => r1_lattices(A,B,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_lattices,d5_lattices,d3_lattices]),
    [file(lattices,t25_lattices),interesting(0.70)]).

fof(t26_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_lattices(A)
        & l2_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( ( r1_lattices(A,B,C)
                  & r1_lattices(A,C,B) )
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_lattices]),
    [file(lattices,t26_lattices),interesting(0.70)]).

fof(t45_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v14_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => r3_lattices(A,B,k6_lattices(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_lattices,t43_lattices]),
    [file(lattices,t45_lattices),interesting(0.68)]).

fof(t50_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v17_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k7_lattices(A,k4_lattices(A,B,C)) = k3_lattices(A,k7_lattices(A,B),k7_lattices(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_lattices,t31_lattices,t48_lattices,t43_lattices,d5_lattices,t48_lattices,d17_lattices,d7_lattices,d11_lattices,t47_lattices,t39_lattices,d7_lattices,t47_lattices,d16_lattices,d18_lattices,d21_lattices]),
    [file(lattices,t50_lattices),interesting(0.66)]).

fof(t52_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v17_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k4_lattices(A,B,C) = k5_lattices(A)
              <=> r3_lattices(A,B,k7_lattices(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t43_lattices,t48_lattices,d11_lattices,t39_lattices,d8_lattices,d3_lattices,t27_lattices,t47_lattices,t41_lattices,t26_lattices]),
    [file(lattices,t52_lattices),interesting(0.66)]).

fof(t51_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v17_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k7_lattices(A,k3_lattices(A,B,C)) = k4_lattices(A,k7_lattices(A,B),k7_lattices(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t49_lattices,t49_lattices,t50_lattices,t49_lattices]),
    [file(lattices,t51_lattices),interesting(0.64)]).

fof(t23_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & v8_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => r1_lattices(A,k4_lattices(A,B,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_lattices,d3_lattices]),
    [file(lattices,t23_lattices),interesting(0.59)]).

fof(t17_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k1_lattices(A,B,B) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d9_lattices,d8_lattices]),
    [file(lattices,t17_lattices),interesting(0.58)]).

fof(t21_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r1_lattices(A,B,C)
              <=> k2_lattices(A,B,C) = B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_lattices,d8_lattices,d9_lattices]),
    [file(lattices,t21_lattices),interesting(0.55)]).

fof(t43_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v14_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k4_lattices(A,k6_lattices(A),B) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattices,d9_lattices]),
    [file(lattices,t43_lattices),interesting(0.54)]).

fof(t31_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v11_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => k3_lattices(A,B,k4_lattices(A,C,D)) = k4_lattices(A,k3_lattices(A,B,C),k3_lattices(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_lattices,t19_lattices]),
    [file(lattices,t31_lattices),interesting(0.54)]).

fof(t39_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v13_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k3_lattices(A,k5_lattices(A),B) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d16_lattices,d8_lattices]),
    [file(lattices,t39_lattices),interesting(0.54)]).

fof(t27_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v7_lattices(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( r1_lattices(A,B,C)
                   => r1_lattices(A,k2_lattices(A,B,D),k2_lattices(A,C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_lattices,d7_lattices,d8_lattices,d3_lattices]),
    [file(lattices,t27_lattices),interesting(0.51)]).

fof(t19_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & l3_lattices(A) )
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k4_lattices(A,B,k3_lattices(A,C,D)) = k3_lattices(A,k4_lattices(A,B,C),k4_lattices(A,B,D)) ) ) )
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k3_lattices(A,B,k4_lattices(A,C,D)) = k4_lattices(A,k3_lattices(A,B,C),k3_lattices(A,B,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_lattices,d5_lattices,d9_lattices,d9_lattices,d7_lattices,d8_lattices]),
    [file(lattices,t19_lattices),interesting(0.49)]).

fof(t48_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v17_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k3_lattices(A,k7_lattices(A,B),B) = k6_lattices(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d21_lattices,d18_lattices]),
    [file(lattices,t48_lattices),interesting(0.47)]).

fof(t47_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v17_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k4_lattices(A,k7_lattices(A,B),B) = k5_lattices(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d21_lattices,d18_lattices]),
    [file(lattices,t47_lattices),interesting(0.47)]).

fof(t22_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v5_lattices(A)
        & v6_lattices(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => r1_lattices(A,B,k1_lattices(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_lattices,t17_lattices,d3_lattices]),
    [file(lattices,t22_lattices),interesting(0.46)]).

fof(t32_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v11_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( ( k4_lattices(A,B,C) = k4_lattices(A,B,D)
                      & k3_lattices(A,B,C) = k3_lattices(A,B,D) )
                   => C = D ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_lattices,d11_lattices,d11_lattices,d9_lattices]),
    [file(lattices,t32_lattices),interesting(0.45)]).

fof(t18_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_lattices(A)
        & v8_lattices(A)
        & v9_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k4_lattices(A,B,B) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d9_lattices,t17_lattices]),
    [file(lattices,t18_lattices),interesting(0.41)]).

fof(l18_lattices,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
        & m2_relset_1(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
            & m2_relset_1(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
         => ( ~ v3_struct_0(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & v10_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & l3_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l4_lattices,d4_lattices,l4_lattices,d5_lattices,l4_lattices,d8_lattices,l4_lattices,d6_lattices,l4_lattices,d7_lattices,l4_lattices,d9_lattices,d10_lattices]),
    [file(lattices,l18_lattices),interesting(0.34)]).

fof(t40_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v13_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k4_lattices(A,k5_lattices(A),B) = k5_lattices(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_lattices]),
    [file(lattices,t40_lattices),interesting(0.34)]).

fof(t44_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v14_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k3_lattices(A,k6_lattices(A),B) = k6_lattices(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattices]),
    [file(lattices,t44_lattices),interesting(0.34)]).

fof(t29_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & l3_lattices(A) )
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k3_lattices(A,k3_lattices(A,k4_lattices(A,B,C),k4_lattices(A,C,D)),k4_lattices(A,D,B)) = k4_lattices(A,k4_lattices(A,k3_lattices(A,B,C),k3_lattices(A,C,D)),k3_lattices(A,D,B)) ) ) )
       => v11_lattices(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_lattices,d7_lattices,d3_lattices,d7_lattices,d5_lattices,t21_lattices,d8_lattices,d11_lattices,d5_lattices,d8_lattices,d8_lattices,d3_lattices,d9_lattices,d7_lattices,d9_lattices,d7_lattices,d7_lattices,d5_lattices,d7_lattices,d5_lattices,d8_lattices]),
    [file(lattices,t29_lattices),interesting(0.32)]).

fof(t34_lattices,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v11_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => k4_lattices(A,k4_lattices(A,k3_lattices(A,B,C),k3_lattices(A,C,D)),k3_lattices(A,D,B)) = k3_lattices(A,k3_lattices(A,k4_lattices(A,B,C),k4_lattices(A,C,D)),k4_lattices(A,D,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_lattices,d7_lattices,d9_lattices,d7_lattices,d9_lattices,d11_lattices,d11_lattices,d5_lattices,d5_lattices,t17_lattices,d5_lattices]),
    [file(lattices,t34_lattices),interesting(0.31)]).

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(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(l4_lattices,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
        & m2_relset_1(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
            & m2_relset_1(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B)))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B)))
                 => C = D ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,t1_zfmisc_1]),
    [file(lattices,l4_lattices),interesting(0.00)]).

fof(d4_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_lattices(A) )
     => ( v4_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k1_lattices(A,B,C) = k1_lattices(A,C,B) ) ) ) ) ),
    file(lattices,d4_lattices),
    [interesting(0.00)]).

fof(d5_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_lattices(A) )
     => ( v5_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k1_lattices(A,B,k1_lattices(A,C,D)) = k1_lattices(A,k1_lattices(A,B,C),D) ) ) ) ) ) ),
    file(lattices,d5_lattices),
    [interesting(0.00)]).

fof(d8_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v8_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k1_lattices(A,k2_lattices(A,B,C),C) = C ) ) ) ) ),
    file(lattices,d8_lattices),
    [interesting(0.00)]).

fof(d6_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_lattices(A) )
     => ( v6_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k2_lattices(A,B,C) = k2_lattices(A,C,B) ) ) ) ) ),
    file(lattices,d6_lattices),
    [interesting(0.00)]).

fof(d7_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_lattices(A) )
     => ( v7_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k2_lattices(A,B,k2_lattices(A,C,D)) = k2_lattices(A,k2_lattices(A,B,C),D) ) ) ) ) ) ),
    file(lattices,d7_lattices),
    [interesting(0.00)]).

fof(d9_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v9_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k2_lattices(A,B,k1_lattices(A,B,C)) = B ) ) ) ) ),
    file(lattices,d9_lattices),
    [interesting(0.00)]).

fof(d10_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v10_lattices(A)
      <=> ( v4_lattices(A)
          & v5_lattices(A)
          & v8_lattices(A)
          & v6_lattices(A)
          & v7_lattices(A)
          & v9_lattices(A) ) ) ) ),
    file(lattices,d10_lattices),
    [interesting(0.00)]).

fof(d1_zfmisc_1,definition,(
    ! [A,B] : 
      ( B = k1_zfmisc_1(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> r1_tarski(C,A) ) ) ),
    file(zfmisc_1,d1_zfmisc_1),
    [interesting(0.00)]).

fof(d13_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_lattices(A) )
     => ( v13_lattices(A)
      <=> ? [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
            & ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( k2_lattices(A,B,C) = B
                  & k2_lattices(A,C,B) = B ) ) ) ) ) ),
    file(lattices,d13_lattices),
    [interesting(0.00)]).

fof(l19_lattices,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
        & m2_relset_1(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
            & m2_relset_1(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
         => ( ~ v3_struct_0(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & v10_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & v13_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & l3_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l18_lattices,d1_zfmisc_1,l4_lattices,d13_lattices]),
    [file(lattices,l19_lattices),interesting(0.00)]).

fof(d14_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_lattices(A) )
     => ( v14_lattices(A)
      <=> ? [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
            & ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( k1_lattices(A,B,C) = B
                  & k1_lattices(A,C,B) = B ) ) ) ) ) ),
    file(lattices,d14_lattices),
    [interesting(0.00)]).

fof(l20_lattices,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
        & m2_relset_1(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
            & m2_relset_1(B,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
         => ( ~ v3_struct_0(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & v10_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & v14_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B))
            & l3_lattices(g3_lattices(k1_zfmisc_1(k1_xboole_0),A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l18_lattices,d1_zfmisc_1,l4_lattices,d14_lattices]),
    [file(lattices,l20_lattices),interesting(0.00)]).

fof(l5_lattices,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
        & m2_relset_1(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(g2_lattices(k1_zfmisc_1(k1_xboole_0),A)))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(g2_lattices(k1_zfmisc_1(k1_xboole_0),A)))
             => B = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,t1_zfmisc_1]),
    [file(lattices,l5_lattices),interesting(0.00)]).

fof(l6_lattices,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0))
        & m2_relset_1(A,k2_zfmisc_1(k1_zfmisc_1(k1_xboole_0),k1_zfmisc_1(k1_xboole_0)),k1_zfmisc_1(k1_xboole_0)) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(g1_lattices(k1_zfmisc_1(k1_xboole_0),A)))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(g1_lattices(k1_zfmisc_1(k1_xboole_0),A)))
             => B = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,t1_zfmisc_1]),
    [file(lattices,l6_lattices),interesting(0.00)]).

fof(t10_lattices,theorem,(
    $true ),
    file(lattices,t10_lattices),
    [interesting(0.00)]).

fof(t11_lattices,theorem,(
    $true ),
    file(lattices,t11_lattices),
    [interesting(0.00)]).

fof(t12_lattices,theorem,(
    $true ),
    file(lattices,t12_lattices),
    [interesting(0.00)]).

fof(t13_lattices,theorem,(
    $true ),
    file(lattices,t13_lattices),
    [interesting(0.00)]).

fof(t14_lattices,theorem,(
    $true ),
    file(lattices,t14_lattices),
    [interesting(0.00)]).

fof(t15_lattices,theorem,(
    $true ),
    file(lattices,t15_lattices),
    [interesting(0.00)]).

fof(t16_lattices,theorem,(
    $true ),
    file(lattices,t16_lattices),
    [interesting(0.00)]).

fof(t1_lattices,theorem,(
    $true ),
    file(lattices,t1_lattices),
    [interesting(0.00)]).

fof(t20_lattices,theorem,(
    $true ),
    file(lattices,t20_lattices),
    [interesting(0.00)]).

fof(t24_lattices,theorem,(
    $true ),
    file(lattices,t24_lattices),
    [interesting(0.00)]).

fof(d3_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r1_lattices(A,B,C)
              <=> k1_lattices(A,B,C) = C ) ) ) ) ),
    file(lattices,d3_lattices),
    [interesting(0.00)]).

fof(t28_lattices,theorem,(
    $true ),
    file(lattices,t28_lattices),
    [interesting(0.00)]).

fof(d11_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v11_lattices(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k2_lattices(A,B,k1_lattices(A,C,D)) = k1_lattices(A,k2_lattices(A,B,C),k2_lattices(A,B,D)) ) ) ) ) ) ),
    file(lattices,d11_lattices),
    [interesting(0.00)]).

fof(t2_lattices,theorem,(
    $true ),
    file(lattices,t2_lattices),
    [interesting(0.00)]).

fof(t30_lattices,theorem,(
    $true ),
    file(lattices,t30_lattices),
    [interesting(0.00)]).

fof(t33_lattices,theorem,(
    $true ),
    file(lattices,t33_lattices),
    [interesting(0.00)]).

fof(t35_lattices,theorem,(
    $true ),
    file(lattices,t35_lattices),
    [interesting(0.00)]).

fof(t36_lattices,theorem,(
    $true ),
    file(lattices,t36_lattices),
    [interesting(0.00)]).

fof(t37_lattices,theorem,(
    $true ),
    file(lattices,t37_lattices),
    [interesting(0.00)]).

fof(t38_lattices,theorem,(
    $true ),
    file(lattices,t38_lattices),
    [interesting(0.00)]).

fof(t3_lattices,theorem,(
    $true ),
    file(lattices,t3_lattices),
    [interesting(0.00)]).

fof(d16_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_lattices(A) )
     => ( v13_lattices(A)
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ( B = k5_lattices(A)
            <=> ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ( k2_lattices(A,B,C) = B
                    & k2_lattices(A,C,B) = B ) ) ) ) ) ) ),
    file(lattices,d16_lattices),
    [interesting(0.00)]).

fof(t42_lattices,theorem,(
    $true ),
    file(lattices,t42_lattices),
    [interesting(0.00)]).

fof(d17_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_lattices(A) )
     => ( v14_lattices(A)
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ( B = k6_lattices(A)
            <=> ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ( k1_lattices(A,B,C) = B
                    & k1_lattices(A,C,B) = B ) ) ) ) ) ) ),
    file(lattices,d17_lattices),
    [interesting(0.00)]).

fof(t46_lattices,theorem,(
    $true ),
    file(lattices,t46_lattices),
    [interesting(0.00)]).

fof(t4_lattices,theorem,(
    $true ),
    file(lattices,t4_lattices),
    [interesting(0.00)]).

fof(d21_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( ( ~ v3_struct_0(A)
              & v10_lattices(A)
              & v11_lattices(A)
              & v16_lattices(A)
              & l3_lattices(A) )
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( C = k7_lattices(A,B)
                <=> r2_lattices(A,C,B) ) ) ) ) ) ),
    file(lattices,d21_lattices),
    [interesting(0.00)]).

fof(d18_lattices,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r2_lattices(A,B,C)
              <=> ( k1_lattices(A,B,C) = k6_lattices(A)
                  & k1_lattices(A,C,B) = k6_lattices(A)
                  & k2_lattices(A,B,C) = k5_lattices(A)
                  & k2_lattices(A,C,B) = k5_lattices(A) ) ) ) ) ) ),
    file(lattices,d18_lattices),
    [interesting(0.00)]).

fof(t5_lattices,theorem,(
    $true ),
    file(lattices,t5_lattices),
    [interesting(0.00)]).

fof(t6_lattices,theorem,(
    $true ),
    file(lattices,t6_lattices),
    [interesting(0.00)]).

fof(t7_lattices,theorem,(
    $true ),
    file(lattices,t7_lattices),
    [interesting(0.00)]).

fof(t8_lattices,theorem,(
    $true ),
    file(lattices,t8_lattices),
    [interesting(0.00)]).

fof(t9_lattices,theorem,(
    $true ),
    file(lattices,t9_lattices),
    [interesting(0.00)]).