theorem :: FILTER_1:46

for L1, L2 being Lattice holds
( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice )