theorem Th40: :: FILTER_1:40

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