theorem Th39: :: FILTER_1:39

for L1, L2 being Lattice holds
( ( L1 is lower-bounded & L2 is lower-bounded ) iff [:L1,L2:] is lower-bounded )