let L1, L2 be Lattice; ( ( 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 )
( [:L1,L2:] is upper-bounded implies ( L1 is upper-bounded & L2 is upper-bounded ) )proof
given p1 being
Element of
L1 such that A1:
for
q1 being
Element of
L1 holds
(
p1 "\/" q1 = p1 &
q1 "\/" p1 = p1 )
;
LATTICES:def 14 ( not L2 is upper-bounded or [:L1,L2:] is upper-bounded )
given p2 being
Element of
L2 such that A2:
for
q2 being
Element of
L2 holds
(
p2 "\/" q2 = p2 &
q2 "\/" p2 = p2 )
;
LATTICES:def 14 [:L1,L2:] is upper-bounded
take a =
[p1,p2];
LATTICES:def 14 for b1 being Element of the carrier of [:L1,L2:] holds
( a "\/" b1 = a & b1 "\/" a = a )
let b be
Element of
[:L1,L2:];
( a "\/" b = a & b "\/" a = a )
consider q1 being
Element of
L1,
q2 being
Element of
L2 such that A3:
b = [q1,q2]
by DOMAIN_1:1;
thus a "\/" b =
[(p1 "\/" q1),(p2 "\/" q2)]
by A3, Th21
.=
[p1,(p2 "\/" q2)]
by A1
.=
a
by A2
;
b "\/" a = a
hence
b "\/" a = a
;
verum
end;
given a being Element of [:L1,L2:] such that A4:
for b being Element of [:L1,L2:] holds
( a "\/" b = a & b "\/" a = a )
; LATTICES:def 14 ( L1 is upper-bounded & L2 is upper-bounded )
consider p1 being Element of L1, p2 being Element of L2 such that
A5:
a = [p1,p2]
by DOMAIN_1:1;
thus
L1 is upper-bounded
L2 is upper-bounded
set q1 = the Element of L1;
take
p2
; LATTICES:def 14 for b1 being Element of the carrier of L2 holds
( p2 "\/" b1 = p2 & b1 "\/" p2 = p2 )
let q2 be Element of L2; ( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 )
a =
a "\/" [ the Element of L1,q2]
by A4
.=
[(p1 "\/" the Element of L1),(p2 "\/" q2)]
by A5, Th21
;
hence
( p2 "\/" q2 = p2 & q2 "\/" p2 = p2 )
by A5, XTUPLE_0:1; verum