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 that
A1: L1 is lower-bounded and
A2: L1 is upper-bounded and
A3: L2 is lower-bounded and
A4: L2 is upper-bounded ; :: according to LATTICES:def 15 :: thesis: [:L1,L2:] is bounded
thus ( [:L1,L2:] is lower-bounded & [:L1,L2:] is upper-bounded ) by A1, A2, A3, A4, Th40, Th41; :: according to LATTICES:def 15 :: thesis: verum

end;

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