theorem :: FILTER_1:34

for L1, L2 being non empty LattStr st [:L1,L2:] is Lattice holds
( L1 is Lattice & L2 is Lattice )