% Mizar problem: t55_tdlat_3,tdlat_3,1712,68 
fof(t55_tdlat_3,conjecture,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ( v4_tdlat_3(A)
      <=> ( ~ v3_struct_0(k4_tdlat_1(A))
          & v10_lattices(k4_tdlat_1(A))
          & v17_lattices(k4_tdlat_1(A))
          & l3_lattices(k4_tdlat_1(A)) ) ) ) ),
    inference(mizar_bg_added,[status(thm)],[cc1_lattices,cc2_lattices,cc3_lattices,cc4_lattices,cc5_lattices,cc6_lattices,cc7_lattices,dt_k12_tdlat_1,dt_k4_tdlat_1,dt_l1_lattices,dt_l1_pre_topc,dt_l1_struct_0,dt_l2_lattices,dt_l3_lattices,existence_l1_lattices,existence_l1_pre_topc,existence_l1_struct_0,existence_l2_lattices,existence_l3_lattices,rc3_struct_0,t46_tdlat_3,t51_tdlat_3]),
    [file(tdlat_3,t55_tdlat_3)]).

fof(cc1_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v10_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v4_lattices(A)
          & v5_lattices(A)
          & v6_lattices(A)
          & v7_lattices(A)
          & v8_lattices(A)
          & v9_lattices(A) ) ) ) ),
    file(lattices,cc1_lattices),
    []).

fof(cc2_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v4_lattices(A)
          & v5_lattices(A)
          & v6_lattices(A)
          & v7_lattices(A)
          & v8_lattices(A)
          & v9_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v10_lattices(A) ) ) ) ),
    file(lattices,cc2_lattices),
    []).

fof(cc3_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v13_lattices(A)
          & v14_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v15_lattices(A) ) ) ) ),
    file(lattices,cc3_lattices),
    []).

fof(cc4_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v15_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v13_lattices(A)
          & v14_lattices(A) ) ) ) ),
    file(lattices,cc4_lattices),
    []).

fof(cc5_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v17_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v11_lattices(A)
          & v13_lattices(A)
          & v14_lattices(A)
          & v15_lattices(A)
          & v16_lattices(A) ) ) ) ),
    file(lattices,cc5_lattices),
    []).

fof(cc6_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v11_lattices(A)
          & v15_lattices(A)
          & v16_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v17_lattices(A) ) ) ) ),
    file(lattices,cc6_lattices),
    []).

fof(cc7_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( ( ~ v3_struct_0(A)
          & v10_lattices(A)
          & v11_lattices(A) )
       => ( ~ v3_struct_0(A)
          & v4_lattices(A)
          & v5_lattices(A)
          & v6_lattices(A)
          & v7_lattices(A)
          & v8_lattices(A)
          & v9_lattices(A)
          & v10_lattices(A)
          & v12_lattices(A) ) ) ) ),
    file(lattices,cc7_lattices),
    []).

fof(dt_k12_tdlat_1,axiom,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ( ~ v3_struct_0(k12_tdlat_1(A))
        & v10_lattices(k12_tdlat_1(A))
        & v17_lattices(k12_tdlat_1(A))
        & l3_lattices(k12_tdlat_1(A)) ) ) ),
    file(tdlat_1,k12_tdlat_1),
    []).

fof(dt_k4_tdlat_1,axiom,(
    ! [A] : 
      ( ( v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ( ~ v3_struct_0(k4_tdlat_1(A))
        & v10_lattices(k4_tdlat_1(A))
        & v15_lattices(k4_tdlat_1(A))
        & v16_lattices(k4_tdlat_1(A))
        & l3_lattices(k4_tdlat_1(A)) ) ) ),
    file(tdlat_1,k4_tdlat_1),
    []).

fof(dt_l1_lattices,axiom,(
    ! [A] : 
      ( l1_lattices(A)
     => l1_struct_0(A) ) ),
    file(lattices,l1_lattices),
    []).

fof(dt_l1_pre_topc,axiom,(
    ! [A] : 
      ( l1_pre_topc(A)
     => l1_struct_0(A) ) ),
    file(pre_topc,l1_pre_topc),
    []).

fof(dt_l1_struct_0,axiom,(
    $true ),
    file(struct_0,l1_struct_0),
    []).

fof(dt_l2_lattices,axiom,(
    ! [A] : 
      ( l2_lattices(A)
     => l1_struct_0(A) ) ),
    file(lattices,l2_lattices),
    []).

fof(dt_l3_lattices,axiom,(
    ! [A] : 
      ( l3_lattices(A)
     => ( l1_lattices(A)
        & l2_lattices(A) ) ) ),
    file(lattices,l3_lattices),
    []).

fof(existence_l1_lattices,axiom,(
    ? [A] : l1_lattices(A) ),
    file(lattices,l1_lattices),
    []).

fof(existence_l1_pre_topc,axiom,(
    ? [A] : l1_pre_topc(A) ),
    file(pre_topc,l1_pre_topc),
    []).

fof(existence_l1_struct_0,axiom,(
    ? [A] : l1_struct_0(A) ),
    file(struct_0,l1_struct_0),
    []).

fof(existence_l2_lattices,axiom,(
    ? [A] : l2_lattices(A) ),
    file(lattices,l2_lattices),
    []).

fof(existence_l3_lattices,axiom,(
    ? [A] : l3_lattices(A) ),
    file(lattices,l3_lattices),
    []).

fof(rc3_struct_0,axiom,(
    ? [A] : 
      ( l1_struct_0(A)
      & ~ v3_struct_0(A) ) ),
    file(struct_0,rc3_struct_0),
    []).

fof(t46_tdlat_3,axiom,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & v4_tdlat_3(A)
        & l1_pre_topc(A) )
     => k4_tdlat_1(A) = k12_tdlat_1(A) ) ),
    file(tdlat_3,t46_tdlat_3),
    []).

fof(t51_tdlat_3,axiom,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_pre_topc(A)
        & l1_pre_topc(A) )
     => ( v4_tdlat_3(A)
      <=> ( ~ v3_struct_0(k4_tdlat_1(A))
          & v10_lattices(k4_tdlat_1(A))
          & v12_lattices(k4_tdlat_1(A))
          & l3_lattices(k4_tdlat_1(A)) ) ) ) ),
    file(tdlat_3,t51_tdlat_3),
    []).