for L1, L2 being Lattice holds
( ( L1 is bounded & L2 is bounded ) iff [:L1,L2:] is bounded ) by Th39, Th40;