let L1, L2 be Lattice; :: thesis: ( ( L1 is bounded & L2 is bounded ) iff [:L1,L2:] is bounded )
thus ( L1 is bounded & L2 is bounded implies [:L1,L2:] is bounded ) :: thesis: ( [:L1,L2:] is bounded implies ( L1 is bounded & L2 is bounded ) )

proof

assume ( L1 is lower-bounded & L1 is upper-bounded & L2 is lower-bounded & L2 is upper-bounded ) ; :: according to LATTICES:def 15 :: thesis: [:L1,L2:] is bounded
hence ( [:L1,L2:] is lower-bounded & [:L1,L2:] is upper-bounded ) by Th40, Th41; :: according to LATTICES:def 15 :: thesis: verum

end;

assume ( [:L1,L2:] is lower-bounded & [:L1,L2:] is upper-bounded ) ; :: according to LATTICES:def 15 :: thesis: ( L1 is bounded & L2 is bounded )
hence ( L1 is lower-bounded & L1 is upper-bounded & L2 is lower-bounded & L2 is upper-bounded ) by Th40, Th41; :: according to LATTICES:def 15 :: thesis: verum