fof(t27_lattice3,theorem,(
    ! [A] : v6_lattice3(k1_lattice3(A)) ),
    inference(mizar_proof,[status(thm)],[d20_lattice3,d3_tarski,t51_lattices,d10_xboole_0,d3_tarski,t51_lattices,t49_lattices,t24_lattice3,t49_lattices,t24_lattice3,t53_lattices,t24_lattice3,t49_lattices,t24_lattice3,t53_lattices,t26_lattice3,d19_lattice3,t50_lattices,t53_lattices]),
    [file(lattice3,t27_lattice3),interesting(1.00)]).

fof(t26_lattice3,theorem,(
    ! [A] : v5_lattice3(k1_lattice3(A)) ),
    inference(mizar_proof,[status(thm)],[d19_lattice3,d1_lattice3,d3_tarski,t17_xboole_1,t95_zfmisc_1,t99_zfmisc_1,d1_lattice3,d3_xboole_0,d3_xboole_0,d17_lattice3,t2_lattice3,t94_zfmisc_1,d17_lattice3,d3_xboole_0,t92_zfmisc_1,t2_lattice3,t2_lattice3,t26_lattices,d17_lattice3,t2_lattice3,t94_zfmisc_1,d17_lattice3,t92_zfmisc_1,t2_lattice3,t2_lattice3,t1_lattice3,t26_lattices,d3_tarski,d3_xboole_0,d4_tarski,d3_xboole_0,d3_xboole_0,t1_lattice3,d3_xboole_0,d4_tarski,t2_lattice3]),
    [file(lattice3,t26_lattice3),interesting(0.88)]).

fof(t25_lattice3,theorem,(
    ! [A] : v4_lattice3(k1_lattice3(A)) ),
    inference(mizar_proof,[status(thm)],[d18_lattice3,t17_xboole_1,t95_zfmisc_1,t99_zfmisc_1,d1_lattice3,d1_lattice3,d17_lattice3,d3_xboole_0,t92_zfmisc_1,t2_lattice3,d17_lattice3,d3_xboole_0,d3_xboole_0,t2_lattice3,t94_zfmisc_1,t2_lattice3]),
    [file(lattice3,t25_lattice3),interesting(0.64)]).

fof(t12_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_orders_2(A) )
     => ( v3_lattice3(A)
       => ( v1_lattice3(A)
          & v2_lattice3(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_lattice3,d10_lattice3,d2_tarski,d9_lattice3,d9_lattice3,d2_tarski,d11_lattice3,d9_lattice3,d9_lattice3,d9_lattice3]),
    [file(lattice3,t12_lattice3),interesting(0.64)]).

fof(t10_lattice3,theorem,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v1_lattice3(A)
      <=> v2_lattice3(k7_lattice3(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_lattice3,d11_lattice3,t9_lattice3,t9_lattice3,t9_lattice3,d11_lattice3,d10_lattice3,t9_lattice3,t9_lattice3,t9_lattice3]),
    [file(lattice3,t10_lattice3),interesting(0.63)]).

fof(t17_lattice3,theorem,(
    ! [A] : 
      ( ( v2_orders_2(A)
        & v4_orders_2(A)
        & v1_lattice3(A)
        & v2_lattice3(A)
        & l1_orders_2(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k13_lattice3(A,k12_lattice3(A,B,C),C) = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_lattice3,d13_lattice3]),
    [file(lattice3,t17_lattice3),interesting(0.59)]).

fof(t18_lattice3,theorem,(
    ! [A] : 
      ( ( v2_orders_2(A)
        & v4_orders_2(A)
        & v1_lattice3(A)
        & v2_lattice3(A)
        & l1_orders_2(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k12_lattice3(A,B,k13_lattice3(A,B,C)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_lattice3,d14_lattice3]),
    [file(lattice3,t18_lattice3),interesting(0.59)]).

fof(t19_lattice3,theorem,(
    ! [A] : 
      ( ( v2_orders_2(A)
        & v3_orders_2(A)
        & v4_orders_2(A)
        & v1_lattice3(A)
        & v2_lattice3(A)
        & l1_orders_2(A) )
     => ? [B] : 
          ( ~ v3_struct_0(B)
          & v3_lattices(B)
          & v10_lattices(B)
          & l3_lattices(B)
          & g1_orders_2(u1_struct_0(A),u1_orders_2(A)) = k3_lattice3(B) ) ) ),
    inference(mizar_proof,[status(thm)],[s7_funct_2,s7_funct_2,t14_lattice3,t17_lattice3,t16_lattice3,t18_lattice3,d4_lattices,d5_lattices,d6_lattices,d7_lattices,d8_lattices,d9_lattices,d10_lattices,d8_filter_1,d2_relat_1,d3_lattices,l26_lattice3,d9_orders_2,t103_zfmisc_1,d9_orders_2,l26_lattice3,t25_orders_2,d3_lattices]),
    [file(lattice3,t19_lattice3),interesting(0.58)]).

fof(t11_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & l3_lattices(A) )
     => ( v1_lattice3(k3_lattice3(A))
        & v2_lattice3(k3_lattice3(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_lattice3,t22_lattices,t7_lattice3,t7_lattice3,t6_filter_0,t7_lattice3,d11_lattice3,t23_lattices,t7_lattice3,t7_lattice3,t7_filter_0,t7_lattice3]),
    [file(lattice3,t11_lattice3),interesting(0.55)]).

fof(t4_lattice3,theorem,(
    ! [A] : 
      ( v14_lattices(k1_lattice3(A))
      & k6_lattices(k1_lattice3(A)) = A ) ),
    inference(mizar_proof,[status(thm)],[d1_lattice3,d1_zfmisc_1,t1_lattice3,t12_xboole_1,d14_lattices,d17_lattices]),
    [file(lattice3,t4_lattice3),interesting(0.53)]).

fof(t49_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( r1_tarski(B,k1_zfmisc_1(u1_struct_0(A)))
         => k15_lattice3(A,k3_tarski(B)) = k15_lattice3(A,a_2_7_lattice3(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,t92_zfmisc_1,t46_lattice3,d21_lattice3,d3_tarski,d4_tarski,t38_lattice3,t46_lattice3,t47_lattice3,t26_lattices]),
    [file(lattice3,t49_lattice3),interesting(0.51)]).

fof(t3_lattice3,theorem,(
    ! [A] : 
      ( v13_lattices(k1_lattice3(A))
      & k5_lattices(k1_lattice3(A)) = k1_xboole_0 ) ),
    inference(mizar_proof,[status(thm)],[t2_xboole_1,d1_lattice3,t1_lattice3,d13_lattices,d16_lattices]),
    [file(lattice3,t3_lattice3),interesting(0.50)]).

fof(t47_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( k15_lattice3(A,B) = k15_lattice3(A,a_2_5_lattice3(A,B))
          & k16_lattice3(A,B) = k16_lattice3(A,a_2_6_lattice3(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,t38_lattice3,d21_lattice3,d17_lattice3,t38_lattice3,t25_lattices,d21_lattice3,t26_lattices,d16_lattice3,t38_lattice3,t34_lattice3,d16_lattice3,t38_lattice3,t25_lattices,t34_lattice3,t26_lattices]),
    [file(lattice3,t47_lattice3),interesting(0.49)]).

fof(t53_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ( ( ~ v3_struct_0(A)
          & v10_lattices(A)
          & v3_filter_0(A)
          & l3_lattices(A) )
       => v5_lattice3(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,t38_lattice3,t52_lattice3,t38_lattice3,d21_lattice3,d8_filter_0,t27_lattices,t25_lattices,t33_lattice3]),
    [file(lattice3,t53_lattice3),interesting(0.49)]).

fof(t35_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : r3_lattices(A,k3_lattices(A,B,k16_lattice3(A,C)),k16_lattice3(A,a_3_4_lattice3(A,B,C))) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_lattice3,t34_lattice3,d16_lattice3,t1_filter_0,t34_lattice3]),
    [file(lattice3,t35_lattice3),interesting(0.48)]).

fof(s1_lattice3,theorem,
    ( ? [A] : 
        ( m1_subset_1(A,f2_s1_lattice3)
        & p1_s1_lattice3(A) )
   => a_0_0_lattice3 = k1_tarski(f1_s1_lattice3) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d1_tarski,d10_xboole_0,d3_tarski,d1_tarski]),
    [file(lattice3,s1_lattice3),interesting(0.48)]).

fof(t5_lattice3,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,u1_struct_0(k1_lattice3(A)))
     => k7_lattices(k1_lattice3(A),B) = k4_xboole_0(A,B) ) ),
    inference(mizar_proof,[status(thm)],[t1_lattice3,t3_lattice3,t4_lattice3,t47_lattices,t48_lattices,d7_xboole_0,t37_xboole_1,t42_xboole_1,t83_xboole_1]),
    [file(lattice3,t5_lattice3),interesting(0.48)]).

fof(t14_lattice3,theorem,(
    ! [A] : 
      ( ( v4_orders_2(A)
        & v1_lattice3(A)
        & l1_orders_2(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))
                 => ( v3_orders_2(A)
                   => k10_lattice3(A,k10_lattice3(A,B,C),D) = k10_lattice3(A,B,k10_lattice3(A,C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_lattice3,t26_orders_2,l26_lattice3,t26_orders_2,l26_lattice3,l26_lattice3,d13_lattice3]),
    [file(lattice3,t14_lattice3),interesting(0.47)]).

fof(t16_lattice3,theorem,(
    ! [A] : 
      ( ( v4_orders_2(A)
        & v2_lattice3(A)
        & l1_orders_2(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))
                 => ( v3_orders_2(A)
                   => k11_lattice3(A,k11_lattice3(A,B,C),D) = k11_lattice3(A,B,k11_lattice3(A,C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_lattice3,t26_orders_2,l28_lattice3,t26_orders_2,l28_lattice3,l28_lattice3,d14_lattice3]),
    [file(lattice3,t16_lattice3),interesting(0.47)]).

fof(t41_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( ( r2_hidden(B,C)
                & r4_lattice3(A,B,C) )
             => k15_lattice3(A,C) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d21_lattice3,t38_lattice3,t26_lattices]),
    [file(lattice3,t41_lattice3),interesting(0.45)]).

fof(t30_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(B))
         => ( r4_lattice3(B,C,A)
          <=> r2_lattice3(k3_lattice3(B),A,k4_lattice3(B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,d9_lattice3,t7_lattice3,d9_lattice3,d17_lattice3,t7_lattice3]),
    [file(lattice3,t30_lattice3),interesting(0.45)]).

fof(t36_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ( v6_lattice3(A)
      <=> ! [B,C] : 
            ( m1_subset_1(C,u1_struct_0(A))
           => r3_lattices(A,k16_lattice3(A,a_3_5_lattice3(A,B,C)),k3_lattices(A,C,k16_lattice3(A,B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d20_lattice3,t34_lattice3,d20_lattice3,t34_lattice3]),
    [file(lattice3,t36_lattice3),interesting(0.44)]).

fof(t31_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(k3_lattice3(B)))
         => ( r2_lattice3(k3_lattice3(B),A,C)
          <=> r4_lattice3(B,k5_lattice3(B,C),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_lattice3]),
    [file(lattice3,t31_lattice3),interesting(0.44)]).

fof(t13_lattice3,theorem,(
    ! [A] : 
      ( ( v4_orders_2(A)
        & v1_lattice3(A)
        & l1_orders_2(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k10_lattice3(A,B,C) = k10_lattice3(A,C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_lattice3,l26_lattice3,d13_lattice3]),
    [file(lattice3,t13_lattice3),interesting(0.43)]).

fof(t15_lattice3,theorem,(
    ! [A] : 
      ( ( v4_orders_2(A)
        & v2_lattice3(A)
        & l1_orders_2(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k11_lattice3(A,B,C) = k11_lattice3(A,C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l28_lattice3,l28_lattice3,d14_lattice3]),
    [file(lattice3,t15_lattice3),interesting(0.43)]).

fof(t2_lattice3,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,u1_struct_0(k1_lattice3(A)))
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(k1_lattice3(A)))
         => ( r1_lattices(k1_lattice3(A),B,C)
          <=> r1_tarski(B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_lattice3,d3_lattices,t7_xboole_1,t12_xboole_1]),
    [file(lattice3,t2_lattice3),interesting(0.43)]).

fof(t24_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & v17_lattices(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(B))
         => ( r3_lattice3(B,C,A)
          <=> r4_lattice3(B,k7_lattices(B,C),a_2_0_lattice3(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_lattice3,d17_lattice3,t53_lattices,d17_lattice3,d16_lattice3,t49_lattices,t53_lattices]),
    [file(lattice3,t24_lattice3),interesting(0.43)]).

fof(t46_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B,C] : 
          ( r1_tarski(B,C)
         => ( r3_lattices(A,k15_lattice3(A,B),k15_lattice3(A,C))
            & r3_lattices(A,k16_lattice3(A,C),k16_lattice3(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,d21_lattice3,d17_lattice3,d21_lattice3,d16_lattice3,t34_lattice3,d16_lattice3,t34_lattice3]),
    [file(lattice3,t46_lattice3),interesting(0.43)]).

fof(s2_lattice3,theorem,
    ( r1_tarski(f2_s2_lattice3,k1_relat_1(f4_s2_lattice3))
   => k9_relat_1(f4_s2_lattice3,a_0_1_lattice3) = a_0_2_lattice3 ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d12_funct_1,d10_xboole_0,d3_tarski,d3_tarski,d12_funct_1]),
    [file(lattice3,s2_lattice3),interesting(0.41)]).

fof(t38_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( r2_hidden(B,C)
             => ( r3_lattices(A,B,k15_lattice3(A,C))
                & r3_lattices(A,k16_lattice3(A,C),B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d21_lattice3,d17_lattice3,d17_lattice3,d16_lattice3,d21_lattice3]),
    [file(lattice3,t38_lattice3),interesting(0.40)]).

fof(t9_lattice3,theorem,(
    ! [A] : 
      ( l1_orders_2(A)
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r1_orders_2(A,B,C)
              <=> r1_orders_2(k7_lattice3(A),k8_lattice3(A,C),k8_lattice3(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_orders_2,d7_relat_1]),
    [file(lattice3,t9_lattice3),interesting(0.39)]).

fof(t32_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : r3_lattices(A,k15_lattice3(A,a_3_2_lattice3(A,B,C)),k4_lattices(A,B,k15_lattice3(A,C))) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,d21_lattice3,d17_lattice3,t27_lattices,d21_lattice3]),
    [file(lattice3,t32_lattice3),interesting(0.39)]).

fof(t33_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ( v5_lattice3(A)
      <=> ! [B,C] : 
            ( m1_subset_1(C,u1_struct_0(A))
           => r3_lattices(A,k4_lattices(A,C,k15_lattice3(A,B)),k15_lattice3(A,a_3_3_lattice3(A,B,C))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d19_lattice3,d21_lattice3,d19_lattice3,d21_lattice3]),
    [file(lattice3,t33_lattice3),interesting(0.38)]).

fof(t37_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : k15_lattice3(A,B) = k16_lattice3(A,a_2_2_lattice3(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d16_lattice3,d21_lattice3,d21_lattice3,d16_lattice3,t34_lattice3]),
    [file(lattice3,t37_lattice3),interesting(0.36)]).

fof(t52_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( ( ~ v3_struct_0(A)
                  & v10_lattices(A)
                  & v3_filter_0(A)
                  & l3_lattices(A) )
               => k4_filter_0(A,B,C) = k15_lattice3(A,a_3_6_lattice3(A,B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_filter_0,d17_lattice3,d8_filter_0,t41_lattice3]),
    [file(lattice3,t52_lattice3),interesting(0.36)]).

fof(t43_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k15_lattice3(A,k1_struct_0(A,B)) = B
            & k16_lattice3(A,k1_struct_0(A,B)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d17_lattice3,d1_tarski,t41_lattice3,d16_lattice3,d1_tarski,t42_lattice3]),
    [file(lattice3,t43_lattice3),interesting(0.35)]).

fof(t45_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( B = k15_lattice3(A,a_2_3_lattice3(A,B))
            & B = k16_lattice3(A,a_2_4_lattice3(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,t41_lattice3,d16_lattice3,t42_lattice3]),
    [file(lattice3,t45_lattice3),interesting(0.35)]).

fof(t7_lattice3,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))
             => ( r3_lattices(A,B,C)
              <=> r3_orders_2(k3_lattice3(A),k4_lattice3(A,B),k4_lattice3(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_filter_1,d9_orders_2]),
    [file(lattice3,t7_lattice3),interesting(0.34)]).

fof(t1_lattice3,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,u1_struct_0(k1_lattice3(A)))
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(k1_lattice3(A)))
         => ( k1_lattices(k1_lattice3(A),B,C) = k2_xboole_0(B,C)
            & k2_lattices(k1_lattice3(A),B,C) = k3_xboole_0(B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_lattice3,d1_lattice3,d1_lattice3]),
    [file(lattice3,t1_lattice3),interesting(0.32)]).

fof(t51_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v14_lattices(A)
        & l3_lattices(A)
        & k6_lattices(A) = k15_lattice3(A,u1_struct_0(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t38_lattice3,t22_lattices,t26_lattices,t26_lattices,d14_lattices,d17_lattices]),
    [file(lattice3,t51_lattice3),interesting(0.31)]).

fof(t23_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & v17_lattices(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(B))
         => ( r4_lattice3(B,C,A)
          <=> r3_lattice3(B,k7_lattices(B,C),a_2_0_lattice3(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,d16_lattice3,t53_lattices,d16_lattice3,d17_lattice3,t49_lattices,t53_lattices]),
    [file(lattice3,t23_lattice3),interesting(0.30)]).

fof(t50_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v13_lattices(A)
        & l3_lattices(A)
        & k5_lattices(A) = k15_lattice3(A,k1_xboole_0) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,d21_lattice3,t23_lattices,t26_lattices,t26_lattices,d13_lattices,d16_lattices]),
    [file(lattice3,t50_lattice3),interesting(0.28)]).

fof(t55_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & v4_lattice3(B)
        & v6_lattice3(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(B))
         => ( k3_lattices(B,C,k16_lattice3(B,A)) = k16_lattice3(B,a_3_9_lattice3(A,B,C))
            & k3_lattices(B,k16_lattice3(B,A),C) = k16_lattice3(B,a_3_10_lattice3(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_lattice3,t36_lattice3,t26_lattices,s5_fraenkel,t26_lattices]),
    [file(lattice3,t55_lattice3),interesting(0.28)]).

fof(t20_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & l3_lattices(A) )
     => ( k6_lattice3(u1_struct_0(A),k2_lattice3(A)) = k2_lattice3(k1_lattice2(A))
        & k7_lattice3(k3_lattice3(A)) = k3_lattice3(k1_lattice2(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_filter_1,d2_lattice2,d2_relat_1,d7_relat_1,t53_lattice2,t33_zfmisc_1,t54_lattice2,t33_zfmisc_1,d7_relat_1]),
    [file(lattice3,t20_lattice3),interesting(0.26)]).

fof(t44_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k3_lattices(A,B,C) = k15_lattice3(A,k2_struct_0(A,B,C))
                & k4_lattices(A,B,C) = k16_lattice3(A,k2_struct_0(A,B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,t22_lattices,d2_tarski,d2_tarski,d17_lattice3,t6_filter_0,d21_lattice3,d16_lattice3,d2_tarski,t23_lattices,d17_lattice3,d16_lattice3,t7_filter_0,t41_lattice3]),
    [file(lattice3,t44_lattice3),interesting(0.25)]).

fof(t21_lattice3,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))
                 => ( r3_lattice3(A,B,k2_struct_0(A,C,D))
                  <=> r3_lattices(A,B,k4_lattices(A,C,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_tarski,d16_lattice3,t7_filter_0,d16_lattice3,t23_lattices,d2_tarski,t25_lattices]),
    [file(lattice3,t21_lattice3),interesting(0.24)]).

fof(t48_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B,C] : 
          ( ! [D] : 
              ( m1_subset_1(D,u1_struct_0(A))
             => ~ ( r2_hidden(D,B)
                  & ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(A))
                     => ~ ( r3_lattices(A,D,E)
                          & r2_hidden(E,C) ) ) ) )
         => r3_lattices(A,k15_lattice3(A,B),k15_lattice3(A,C)) ) ) ),
    inference(mizar_proof,[status(thm)],[d17_lattice3,t38_lattice3,t25_lattices,d21_lattice3]),
    [file(lattice3,t48_lattice3),interesting(0.24)]).

fof(t22_lattice3,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))
                 => ( r4_lattice3(A,B,k2_struct_0(A,C,D))
                  <=> r3_lattices(A,k3_lattices(A,C,D),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_tarski,d17_lattice3,t6_filter_0,d17_lattice3,t22_lattices,d2_tarski,t25_lattices]),
    [file(lattice3,t22_lattice3),interesting(0.23)]).

fof(l80_lattice3,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k1_zfmisc_1(A),A)
            & m2_relset_1(B,k1_zfmisc_1(A),A) )
         => ~ ( ! [C] : 
                  ( m1_subset_1(C,A)
                 => k8_funct_2(k1_zfmisc_1(A),A,B,k6_domain_1(A,C)) = C )
              & ! [C] : 
                  ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
                 => k8_funct_2(k1_zfmisc_1(A),A,B,k10_relset_1(k1_zfmisc_1(A),A,B,C)) = k1_funct_1(B,k3_tarski(C)) )
              & ! [C] : 
                  ( ( ~ v3_struct_0(C)
                    & v3_lattices(C)
                    & v10_lattices(C)
                    & l3_lattices(C) )
                 => ~ ( u1_struct_0(C) = A
                      & ! [D] : 
                          ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(C)))
                         => k15_lattice3(C,D) = k1_funct_1(B,D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s1_relset_1,d1_funct_2,t118_funct_1,t93_zfmisc_1,d3_tarski,d2_xboole_0,d1_tarski,d2_tarski,d4_tarski,d10_xboole_0,d3_tarski,d4_tarski,d1_tarski,d2_tarski,d2_xboole_0,d3_tarski,t92_zfmisc_1,t1_xboole_1,d1_funct_2,s2_lattice3,d1_relat_2,t69_enumset1,d4_relat_2,d8_relat_2,t42_enumset1,t43_enumset1,t98_orders_1,t98_orders_1,d4_partfun1,d9_relat_2,d12_relat_2,d16_relat_2,d12_lattice3,t17_xboole_1,d9_lattice3,d3_xboole_0,t46_zfmisc_1,d9_orders_2,d3_tarski,d3_xboole_0,d9_lattice3,d9_orders_2,s6_fraenkel,s1_lattice3,d9_orders_2,t12_lattice3,d15_lattice3,d15_lattice3,d9_lattice3,d15_lattice3,t46_zfmisc_1,d9_orders_2,t31_lattice3,t30_lattice3,d3_tarski,d15_lattice3,d9_lattice3,d9_orders_2,s6_fraenkel,s1_lattice3,d9_orders_2,t7_lattice3,d21_lattice3]),
    [file(lattice3,l80_lattice3),interesting(0.23)]).

fof(t42_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( ( r2_hidden(B,C)
                & r3_lattice3(A,B,C) )
             => k16_lattice3(A,C) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t38_lattice3,t40_lattice3,t26_lattices]),
    [file(lattice3,t42_lattice3),interesting(0.20)]).

fof(t40_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( r3_lattice3(A,B,C)
             => r3_lattices(A,B,k16_lattice3(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t38_lattice3]),
    [file(lattice3,t40_lattice3),interesting(0.19)]).

fof(t54_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & v4_lattice3(B)
        & v5_lattice3(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(B))
         => ( k4_lattices(B,C,k15_lattice3(B,A)) = k15_lattice3(B,a_3_7_lattice3(A,B,C))
            & k4_lattices(B,k15_lattice3(B,A),C) = k15_lattice3(B,a_3_8_lattice3(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_lattice3,t33_lattice3,t26_lattices,s5_fraenkel,t26_lattices]),
    [file(lattice3,t54_lattice3),interesting(0.19)]).

fof(t28_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(B))
         => ( r3_lattice3(B,C,A)
          <=> r1_lattice3(k3_lattice3(B),A,k4_lattice3(B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_lattice3,d8_lattice3,t7_lattice3,d8_lattice3,d16_lattice3,t7_lattice3]),
    [file(lattice3,t28_lattice3),interesting(0.18)]).

fof(t34_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & v4_lattice3(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( B = k16_lattice3(A,C)
            <=> ( r3_lattice3(A,B,C)
                & ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( r3_lattice3(A,D,C)
                     => r3_lattices(A,D,B) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d21_lattice3,d21_lattice3,d16_lattice3,d17_lattice3,d16_lattice3,d21_lattice3,d17_lattice3,d17_lattice3,d17_lattice3]),
    [file(lattice3,t34_lattice3),interesting(0.09)]).

fof(t56_lattice3,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k1_zfmisc_1(A),A)
            & m2_relset_1(B,k1_zfmisc_1(A),A) )
         => ~ ( ! [C] : 
                  ( m1_subset_1(C,A)
                 => k8_funct_2(k1_zfmisc_1(A),A,B,k6_domain_1(A,C)) = C )
              & ! [C] : 
                  ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(A)))
                 => k8_funct_2(k1_zfmisc_1(A),A,B,k10_relset_1(k1_zfmisc_1(A),A,B,C)) = k1_funct_1(B,k3_tarski(C)) )
              & ! [C] : 
                  ( ( ~ v3_struct_0(C)
                    & v3_lattices(C)
                    & v10_lattices(C)
                    & v4_lattice3(C)
                    & l3_lattices(C) )
                 => ~ ( u1_struct_0(C) = A
                      & ! [D] : 
                          ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(C)))
                         => k15_lattice3(C,D) = k1_funct_1(B,D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l80_lattice3]),
    [file(lattice3,t56_lattice3),interesting(0.06)]).

fof(d10_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v1_lattice3(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_orders_2(A,B,D)
                    & r1_orders_2(A,C,D)
                    & ! [E] : 
                        ( m1_subset_1(E,u1_struct_0(A))
                       => ( ( r1_orders_2(A,B,E)
                            & r1_orders_2(A,C,E) )
                         => r1_orders_2(A,D,E) ) ) ) ) ) ) ) ),
    file(lattice3,d10_lattice3),
    [interesting(0.00)]).

fof(d11_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v2_lattice3(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_orders_2(A,D,B)
                    & r1_orders_2(A,D,C)
                    & ! [E] : 
                        ( m1_subset_1(E,u1_struct_0(A))
                       => ( ( r1_orders_2(A,E,B)
                            & r1_orders_2(A,E,C) )
                         => r1_orders_2(A,E,D) ) ) ) ) ) ) ) ),
    file(lattice3,d11_lattice3),
    [interesting(0.00)]).

fof(d9_orders_2,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( r1_orders_2(A,B,C)
              <=> r2_hidden(k4_tarski(B,C),u1_orders_2(A)) ) ) ) ) ),
    file(orders_2,d9_orders_2),
    [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(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)) ) ) ) ),
    file(lattices,t22_lattices),
    [interesting(0.00)]).

fof(t32_filter_1,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))
             => ( r2_hidden(k1_domain_1(u1_struct_0(A),u1_struct_0(A),B,C),k9_filter_1(A))
              <=> r3_lattices(A,B,C) ) ) ) ) ),
    file(filter_1,t32_filter_1),
    [interesting(0.00)]).

fof(t6_filter_0,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))
                 => ( ( r3_lattices(A,B,C)
                      & r3_lattices(A,D,C) )
                   => r3_lattices(A,k3_lattices(A,B,D),C) ) ) ) ) ) ),
    file(filter_0,t6_filter_0),
    [interesting(0.00)]).

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) ) ) ) ),
    file(lattices,t23_lattices),
    [interesting(0.00)]).

fof(t7_filter_0,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))
                 => ( ( r3_lattices(A,B,C)
                      & r3_lattices(A,B,D) )
                   => r3_lattices(A,B,k4_lattices(A,C,D)) ) ) ) ) ) ),
    file(filter_0,t7_filter_0),
    [interesting(0.00)]).

fof(d13_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v4_orders_2(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_orders_2(A,B,D)
                      & r1_orders_2(A,C,D)
                      & ! [E] : 
                          ( m1_subset_1(E,u1_struct_0(A))
                         => ( ( r1_orders_2(A,B,E)
                              & r1_orders_2(A,C,E) )
                           => r1_orders_2(A,D,E) ) ) )
                 => ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => ( D = k10_lattice3(A,B,C)
                      <=> ( r1_orders_2(A,B,D)
                          & r1_orders_2(A,C,D)
                          & ! [E] : 
                              ( m1_subset_1(E,u1_struct_0(A))
                             => ( ( r1_orders_2(A,B,E)
                                  & r1_orders_2(A,C,E) )
                               => r1_orders_2(A,D,E) ) ) ) ) ) ) ) ) ) ) ),
    file(lattice3,d13_lattice3),
    [interesting(0.00)]).

fof(l26_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_orders_2(A)
        & v1_lattice3(A)
        & l1_orders_2(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))
                 => ( D = k10_lattice3(A,B,C)
                  <=> ( r1_orders_2(A,B,D)
                      & r1_orders_2(A,C,D)
                      & ! [E] : 
                          ( m1_subset_1(E,u1_struct_0(A))
                         => ( ( r1_orders_2(A,B,E)
                              & r1_orders_2(A,C,E) )
                           => r1_orders_2(A,D,E) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_lattice3,d13_lattice3]),
    [file(lattice3,l26_lattice3),interesting(0.00)]).

fof(d14_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v4_orders_2(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_orders_2(A,D,B)
                      & r1_orders_2(A,D,C)
                      & ! [E] : 
                          ( m1_subset_1(E,u1_struct_0(A))
                         => ( ( r1_orders_2(A,E,B)
                              & r1_orders_2(A,E,C) )
                           => r1_orders_2(A,E,D) ) ) )
                 => ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => ( D = k11_lattice3(A,B,C)
                      <=> ( r1_orders_2(A,D,B)
                          & r1_orders_2(A,D,C)
                          & ! [E] : 
                              ( m1_subset_1(E,u1_struct_0(A))
                             => ( ( r1_orders_2(A,E,B)
                                  & r1_orders_2(A,E,C) )
                               => r1_orders_2(A,E,D) ) ) ) ) ) ) ) ) ) ) ),
    file(lattice3,d14_lattice3),
    [interesting(0.00)]).

fof(l28_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_orders_2(A)
        & v2_lattice3(A)
        & l1_orders_2(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))
                 => ( D = k11_lattice3(A,B,C)
                  <=> ( r1_orders_2(A,D,B)
                      & r1_orders_2(A,D,C)
                      & ! [E] : 
                          ( m1_subset_1(E,u1_struct_0(A))
                         => ( ( r1_orders_2(A,E,B)
                              & r1_orders_2(A,E,C) )
                           => r1_orders_2(A,E,D) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_lattice3,d14_lattice3]),
    [file(lattice3,l28_lattice3),interesting(0.00)]).

fof(s7_funct_2,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s7_funct_2)
       => ! [B] : 
            ( m1_subset_1(B,f2_s7_funct_2)
           => ? [C] : 
                ( m1_subset_1(C,f3_s7_funct_2)
                & p1_s7_funct_2(A,B,C) ) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(f1_s7_funct_2,f2_s7_funct_2),f3_s7_funct_2)
        & m2_relset_1(A,k2_zfmisc_1(f1_s7_funct_2,f2_s7_funct_2),f3_s7_funct_2)
        & ! [B] : 
            ( m1_subset_1(B,f1_s7_funct_2)
           => ! [C] : 
                ( m1_subset_1(C,f2_s7_funct_2)
               => p1_s7_funct_2(B,C,k1_funct_1(A,k4_tarski(B,C))) ) ) ) ),
    file(funct_2,s7_funct_2),
    [interesting(0.00)]).

fof(t26_orders_2,theorem,(
    ! [A] : 
      ( ( v3_orders_2(A)
        & l1_orders_2(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_orders_2(A,B,C)
                      & r1_orders_2(A,C,D) )
                   => r1_orders_2(A,B,D) ) ) ) ) ) ),
    file(orders_2,t26_orders_2),
    [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(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(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(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(d8_filter_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & l3_lattices(A) )
     => k9_filter_1(A) = a_1_0_filter_1(A) ) ),
    file(filter_1,d8_filter_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(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(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(t25_orders_2,theorem,(
    ! [A] : 
      ( ( v4_orders_2(A)
        & l1_orders_2(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( ( r1_orders_2(A,B,C)
                  & r1_orders_2(A,C,B) )
               => B = C ) ) ) ) ),
    file(orders_2,t25_orders_2),
    [interesting(0.00)]).

fof(d2_lattice2,definition,(
    ! [A] : 
      ( l3_lattices(A)
     => k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ) ),
    file(lattice2,d2_lattice2),
    [interesting(0.00)]).

fof(t53_lattice2,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))
             => ( r3_lattices(A,B,C)
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(k1_lattice2(A)))
                   => ! [E] : 
                        ( m1_subset_1(E,u1_struct_0(k1_lattice2(A)))
                       => ( ( B = D
                            & C = E )
                         => r3_lattices(k1_lattice2(A),E,D) ) ) ) ) ) ) ) ),
    file(lattice2,t53_lattice2),
    [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(t54_lattice2,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(k1_lattice2(A)))
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(k1_lattice2(A)))
                     => ( ( r3_lattices(k1_lattice2(A),D,E)
                          & B = D
                          & C = E )
                       => r3_lattices(A,C,B) ) ) ) ) ) ) ),
    file(lattice2,t54_lattice2),
    [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(d16_lattice3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( r3_lattice3(A,B,C)
            <=> ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( r2_hidden(D,C)
                   => r1_lattices(A,B,D) ) ) ) ) ) ),
    file(lattice3,d16_lattice3),
    [interesting(0.00)]).

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) ) ) ) ) ) ),
    file(lattices,t25_lattices),
    [interesting(0.00)]).

fof(d17_lattice3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( r4_lattice3(A,B,C)
            <=> ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( r2_hidden(D,C)
                   => r1_lattices(A,D,B) ) ) ) ) ) ),
    file(lattice3,d17_lattice3),
    [interesting(0.00)]).

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)) ) ) ) ) ),
    file(lattices,t53_lattices),
    [interesting(0.00)]).

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 ) ) ),
    file(lattices,t49_lattices),
    [interesting(0.00)]).

fof(d18_lattice3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v4_lattice3(A)
      <=> ! [B] : 
          ? [C] : 
            ( m1_subset_1(C,u1_struct_0(A))
            & r4_lattice3(A,C,B)
            & ! [D] : 
                ( m1_subset_1(D,u1_struct_0(A))
               => ( r4_lattice3(A,D,B)
                 => r1_lattices(A,C,D) ) ) ) ) ) ),
    file(lattice3,d18_lattice3),
    [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(t95_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => r1_tarski(k3_tarski(A),k3_tarski(B)) ) ),
    file(zfmisc_1,t95_zfmisc_1),
    [interesting(0.00)]).

fof(t99_zfmisc_1,theorem,(
    ! [A] : k3_tarski(k1_zfmisc_1(A)) = A ),
    file(zfmisc_1,t99_zfmisc_1),
    [interesting(0.00)]).

fof(d1_lattice3,definition,(
    ! [A,B] : 
      ( ( v3_lattices(B)
        & l3_lattices(B) )
     => ( B = k1_lattice3(A)
      <=> ( u1_struct_0(B) = k1_zfmisc_1(A)
          & ! [C] : 
              ( m1_subset_1(C,k1_zfmisc_1(A))
             => ! [D] : 
                  ( m1_subset_1(D,k1_zfmisc_1(A))
                 => ( k1_binop_1(u2_lattices(B),C,D) = k4_subset_1(A,C,D)
                    & k1_binop_1(u1_lattices(B),C,D) = k5_subset_1(A,C,D) ) ) ) ) ) ) ),
    file(lattice3,d1_lattice3),
    [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(t92_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => r1_tarski(A,k3_tarski(B)) ) ),
    file(zfmisc_1,t92_zfmisc_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(t12_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => k2_xboole_0(A,B) = B ) ),
    file(xboole_1,t12_xboole_1),
    [interesting(0.00)]).

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

fof(d20_lattice3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v6_lattice3(A)
      <=> ! [B,C] : 
            ( m1_subset_1(C,u1_struct_0(A))
           => ! [D] : 
                ( m1_subset_1(D,u1_struct_0(A))
               => ! [E] : 
                    ( m1_subset_1(E,u1_struct_0(A))
                   => ( ( r3_lattice3(A,C,B)
                        & ! [F] : 
                            ( m1_subset_1(F,u1_struct_0(A))
                           => ( r3_lattice3(A,F,B)
                             => r1_lattices(A,F,C) ) )
                        & r3_lattice3(A,E,a_3_1_lattice3(A,B,D))
                        & ! [F] : 
                            ( m1_subset_1(F,u1_struct_0(A))
                           => ( r3_lattice3(A,F,a_3_1_lattice3(A,B,D))
                             => r1_lattices(A,F,E) ) ) )
                     => r1_lattices(A,E,k1_lattices(A,D,C)) ) ) ) ) ) ) ),
    file(lattice3,d20_lattice3),
    [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(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)) ) ) ) ),
    file(lattices,t51_lattices),
    [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(d19_lattice3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( v5_lattice3(A)
      <=> ! [B,C] : 
            ( m1_subset_1(C,u1_struct_0(A))
           => ! [D] : 
                ( m1_subset_1(D,u1_struct_0(A))
               => ! [E] : 
                    ( m1_subset_1(E,u1_struct_0(A))
                   => ( ( r4_lattice3(A,C,B)
                        & ! [F] : 
                            ( m1_subset_1(F,u1_struct_0(A))
                           => ( r4_lattice3(A,F,B)
                             => r1_lattices(A,C,F) ) )
                        & r4_lattice3(A,E,a_3_0_lattice3(A,B,D))
                        & ! [F] : 
                            ( m1_subset_1(F,u1_struct_0(A))
                           => ( r4_lattice3(A,F,a_3_0_lattice3(A,B,D))
                             => r1_lattices(A,E,F) ) ) )
                     => r1_lattices(A,k2_lattices(A,D,C),E) ) ) ) ) ) ) ),
    file(lattice3,d19_lattice3),
    [interesting(0.00)]).

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 ) ) ) ) ),
    file(lattices,t26_lattices),
    [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(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)) ) ) ) ),
    file(lattices,t50_lattices),
    [interesting(0.00)]).

fof(d8_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ! [B,C] : 
          ( m1_subset_1(C,u1_struct_0(A))
         => ( r1_lattice3(A,B,C)
          <=> ! [D] : 
                ( m1_subset_1(D,u1_struct_0(A))
               => ( r2_hidden(D,B)
                 => r1_orders_2(A,C,D) ) ) ) ) ) ),
    file(lattice3,d8_lattice3),
    [interesting(0.00)]).

fof(t29_lattice3,theorem,(
    ! [A,B] : 
      ( ( ~ v3_struct_0(B)
        & v10_lattices(B)
        & l3_lattices(B) )
     => ! [C] : 
          ( m1_subset_1(C,u1_struct_0(k3_lattice3(B)))
         => ( r1_lattice3(k3_lattice3(B),A,C)
          <=> r3_lattice3(B,k5_lattice3(B,C),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_lattice3]),
    [file(lattice3,t29_lattice3),interesting(0.00)]).

fof(d21_lattice3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_lattices(A) )
     => ( ( ~ v3_struct_0(A)
          & v10_lattices(A)
          & v4_lattice3(A)
          & l3_lattices(A) )
       => ! [B,C] : 
            ( m1_subset_1(C,u1_struct_0(A))
           => ( C = k15_lattice3(A,B)
            <=> ( r4_lattice3(A,C,B)
                & ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( r4_lattice3(A,D,B)
                     => r1_lattices(A,C,D) ) ) ) ) ) ) ) ),
    file(lattice3,d21_lattice3),
    [interesting(0.00)]).

fof(t39_lattice3,theorem,(
    $true ),
    file(lattice3,t39_lattice3),
    [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(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(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(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(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(d8_filter_0,definition,(
    ! [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))
             => ( ( ~ v3_struct_0(A)
                  & v10_lattices(A)
                  & v3_filter_0(A)
                  & l3_lattices(A) )
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( D = k4_filter_0(A,B,C)
                    <=> ( r3_lattices(A,k4_lattices(A,B,D),C)
                        & ! [E] : 
                            ( m1_subset_1(E,u1_struct_0(A))
                           => ( r3_lattices(A,k4_lattices(A,B,E),C)
                             => r3_lattices(A,E,D) ) ) ) ) ) ) ) ) ) ),
    file(filter_0,d8_filter_0),
    [interesting(0.00)]).

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)) ) ) ) ) ) ),
    file(lattices,t27_lattices),
    [interesting(0.00)]).

fof(s5_fraenkel,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s5_fraenkel)
       => f2_s5_fraenkel(A) = f3_s5_fraenkel(A) )
   => a_0_8_fraenkel = a_0_9_fraenkel ),
    file(fraenkel,s5_fraenkel),
    [interesting(0.00)]).

fof(t1_filter_0,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))
                 => ( r3_lattices(A,B,C)
                   => ( r3_lattices(A,k3_lattices(A,D,B),k3_lattices(A,D,C))
                      & r3_lattices(A,k3_lattices(A,B,D),k3_lattices(A,C,D))
                      & r3_lattices(A,k3_lattices(A,B,D),k3_lattices(A,D,C))
                      & r3_lattices(A,k3_lattices(A,D,B),k3_lattices(A,C,D)) ) ) ) ) ) ) ),
    file(filter_0,t1_filter_0),
    [interesting(0.00)]).

fof(s1_relset_1,theorem,(
    ? [A] : 
      ( m2_relset_1(A,f1_s1_relset_1,f2_s1_relset_1)
      & ! [B,C] : 
          ( r2_hidden(k4_tarski(B,C),A)
        <=> ( r2_hidden(B,f1_s1_relset_1)
            & r2_hidden(C,f2_s1_relset_1)
            & p1_s1_relset_1(B,C) ) ) ) ),
    file(relset_1,s1_relset_1),
    [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(t118_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( ( r2_hidden(A,k1_relat_1(C))
          & r2_hidden(B,k1_relat_1(C)) )
       => k9_relat_1(C,k2_tarski(A,B)) = k2_tarski(k1_funct_1(C,A),k1_funct_1(C,B)) ) ) ),
    file(funct_1,t118_funct_1),
    [interesting(0.00)]).

fof(t93_zfmisc_1,theorem,(
    ! [A,B] : k3_tarski(k2_tarski(A,B)) = k2_xboole_0(A,B) ),
    file(zfmisc_1,t93_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(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(d12_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( C = k9_relat_1(A,B)
        <=> ! [D] : 
              ( r2_hidden(D,C)
            <=> ? [E] : 
                  ( r2_hidden(E,k1_relat_1(A))
                  & r2_hidden(E,B)
                  & D = k1_funct_1(A,E) ) ) ) ) ),
    file(funct_1,d12_funct_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(t69_enumset1,theorem,(
    ! [A] : k2_tarski(A,A) = k1_tarski(A) ),
    file(enumset1,t69_enumset1),
    [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(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(t42_enumset1,theorem,(
    ! [A,B,C] : k1_enumset1(A,B,C) = k2_xboole_0(k1_tarski(A),k2_tarski(B,C)) ),
    file(enumset1,t42_enumset1),
    [interesting(0.00)]).

fof(t43_enumset1,theorem,(
    ! [A,B,C] : k1_enumset1(A,B,C) = k2_xboole_0(k2_tarski(A,B),k1_tarski(C)) ),
    file(enumset1,t43_enumset1),
    [interesting(0.00)]).

fof(t98_orders_1,theorem,(
    ! [A,B] : 
      ( m2_relset_1(B,A,A)
     => ( r1_relat_2(B,A)
       => ( k4_relset_1(A,A,B) = A
          & k3_relat_1(B) = A ) ) ) ),
    file(orders_1,t98_orders_1),
    [interesting(0.00)]).

fof(d4_partfun1,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( v1_partfun1(C,A,B)
      <=> k4_relset_1(A,B,C) = A ) ) ),
    file(partfun1,d4_partfun1),
    [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(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(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(d12_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( v3_lattice3(A)
      <=> ! [B] : 
          ? [C] : 
            ( m1_subset_1(C,u1_struct_0(A))
            & r2_lattice3(A,B,C)
            & ! [D] : 
                ( m1_subset_1(D,u1_struct_0(A))
               => ( r2_lattice3(A,B,D)
                 => r1_orders_2(A,C,D) ) ) ) ) ) ),
    file(lattice3,d12_lattice3),
    [interesting(0.00)]).

fof(d9_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ! [B,C] : 
          ( m1_subset_1(C,u1_struct_0(A))
         => ( r2_lattice3(A,B,C)
          <=> ! [D] : 
                ( m1_subset_1(D,u1_struct_0(A))
               => ( r2_hidden(D,B)
                 => r1_orders_2(A,D,C) ) ) ) ) ) ),
    file(lattice3,d9_lattice3),
    [interesting(0.00)]).

fof(t46_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r2_hidden(A,B)
     => k2_xboole_0(k1_tarski(A),B) = B ) ),
    file(zfmisc_1,t46_zfmisc_1),
    [interesting(0.00)]).

fof(s6_fraenkel,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s6_fraenkel)
       => ( p1_s6_fraenkel(A)
         => f2_s6_fraenkel(A) = f3_s6_fraenkel(A) ) )
   => a_0_10_fraenkel = a_0_11_fraenkel ),
    file(fraenkel,s6_fraenkel),
    [interesting(0.00)]).

fof(d15_lattice3,definition,(
    ! [A] : 
      ( l1_orders_2(A)
     => ( ( v2_orders_2(A)
          & v3_orders_2(A)
          & v4_orders_2(A)
          & v1_lattice3(A)
          & v2_lattice3(A)
          & l1_orders_2(A) )
       => ! [B] : 
            ( ( ~ v3_struct_0(B)
              & v3_lattices(B)
              & v10_lattices(B)
              & l3_lattices(B) )
           => ( B = k14_lattice3(A)
            <=> g1_orders_2(u1_struct_0(A),u1_orders_2(A)) = k3_lattice3(B) ) ) ) ) ),
    file(lattice3,d15_lattice3),
    [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_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(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) ) ) ),
    file(lattices,t47_lattices),
    [interesting(0.00)]).

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) ) ) ),
    file(lattices,t48_lattices),
    [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(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(t42_xboole_1,theorem,(
    ! [A,B,C] : k4_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(k4_xboole_0(A,C),k4_xboole_0(B,C)) ),
    file(xboole_1,t42_xboole_1),
    [interesting(0.00)]).

fof(t83_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_xboole_0(A,B)
    <=> k4_xboole_0(A,B) = A ) ),
    file(xboole_1,t83_xboole_1),
    [interesting(0.00)]).

fof(t2_binop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,B),C)
                    & m2_relset_1(D,k2_zfmisc_1(A,B),C) )
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k2_zfmisc_1(A,B),C)
                        & m2_relset_1(E,k2_zfmisc_1(A,B),C) )
                     => ( ! [F] : 
                            ( m1_subset_1(F,A)
                           => ! [G] : 
                                ( m1_subset_1(G,B)
                               => k2_binop_1(A,B,C,D,F,G) = k2_binop_1(A,B,C,E,F,G) ) )
                       => D = E ) ) ) ) ) ) ),
    file(binop_1,t2_binop_1),
    [interesting(0.00)]).

fof(t6_lattice3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v10_lattices(A)
        & l3_lattices(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v10_lattices(B)
            & l3_lattices(B) )
         => ( k3_lattice3(A) = k3_lattice3(B)
           => g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t22_lattices,t32_filter_1,t32_filter_1,t6_filter_0,t32_filter_1,t32_filter_1,t26_lattices,t2_binop_1,t23_lattices,t32_filter_1,t32_filter_1,t7_filter_0,t32_filter_1,t32_filter_1,t26_lattices,t2_binop_1]),
    [file(lattice3,t6_lattice3),interesting(0.00)]).

fof(t8_lattice3,theorem,(
    ! [A] : 
      ( l1_orders_2(A)
     => k7_lattice3(k7_lattice3(A)) = g1_orders_2(u1_struct_0(A),u1_orders_2(A)) ) ),
    file(lattice3,t8_lattice3),
    [interesting(0.00)]).