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

proof

given p1 being Element of such that A1: for q1 being Element of holds
( p1 "\/" q1 = p1 & q1 "\/" p1 = p1 ) ; :: according to LATTICES:def 14 :: thesis: ( not L2 is upper-bounded or [:L1,L2:] is upper-bounded )
given p2 being Element of such that A2: for q2 being Element of holds
( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 ) ; :: according to LATTICES:def 14 :: thesis: [:L1,L2:] is upper-bounded
take a = [p1,p2]; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of [:L1,L2:] holds
( a "\/" b₁ = a & b₁ "\/" a = a )
let b be Element of ; :: thesis: ( a "\/" b = a & b "\/" a = a )
consider q1 being Element of , q2 being Element of such that
A3: b = [q1,q2] by DOMAIN_1:9;
thus a "\/" b = [(p1 "\/" q1),(p2 "\/" q2)] by A3, Th22
.= [p1,(p2 "\/" q2)] by A1
.= a by A2 ; :: thesis: b "\/" a = a
hence b "\/" a = a ; :: thesis: verum

end;

given a being Element of such that A4: for b being Element of holds
( a "\/" b = a & b "\/" a = a ) ; :: according to LATTICES:def 14 :: thesis: ( L1 is upper-bounded & L2 is upper-bounded )
consider p1 being Element of , p2 being Element of such that
A5: a = [p1,p2] by DOMAIN_1:9;
thus L1 is upper-bounded :: thesis: L2 is upper-bounded

proof

consider q2 being Element of ;
take p1 ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of L1 holds
( p1 "\/" b₁ = p1 & b₁ "\/" p1 = p1 )
let q1 be Element of ; :: thesis: ( p1 "\/" q1 = p1 & q1 "\/" p1 = p1 )
a = a "\/" [q1,q2] by A4
.= [(p1 "\/" q1),(p2 "\/" q2)] by A5, Th22 ;
hence ( p1 "\/" q1 = p1 & q1 "\/" p1 = p1 ) by A5, ZFMISC_1:33; :: thesis: verum

end;

consider q1 being Element of ;
take p2 ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of L2 holds
( p2 "\/" b₁ = p2 & b₁ "\/" p2 = p2 )
let q2 be Element of ; :: thesis: ( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 )
a = a "\/" [q1,q2] by A4
.= [(p1 "\/" q1),(p2 "\/" q2)] by A5, Th22 ;
hence ( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 ) by A5, ZFMISC_1:33; :: thesis: verum