let L1, L2 be Lattice; :: thesis: ( ( L1 is lower-bounded & L2 is lower-bounded ) iff [:L1,L2:] is lower-bounded )
thus
( L1 is lower-bounded & L2 is lower-bounded implies [:L1,L2:] is lower-bounded )
:: thesis: ( [:L1,L2:] is lower-bounded implies ( L1 is lower-bounded & L2 is lower-bounded ) )proof
given p1 being
Element of
L1 such that A1:
for
q1 being
Element of
L1 holds
(
p1 "/\" q1 = p1 &
q1 "/\" p1 = p1 )
;
:: according to LATTICES:def 13 :: thesis: ( not L2 is lower-bounded or [:L1,L2:] is lower-bounded )
given p2 being
Element of
L2 such that A2:
for
q2 being
Element of
L2 holds
(
p2 "/\" q2 = p2 &
q2 "/\" p2 = p2 )
;
:: according to LATTICES:def 13 :: thesis: [:L1,L2:] is lower-bounded
take a =
[p1,p2];
:: according to LATTICES:def 13 :: thesis: for b1 being Element of the carrier of [:L1,L2:] holds
( a "/\" b1 = a & b1 "/\" a = a )
let b be
Element of
[:L1,L2:];
:: thesis: ( 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: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 [:L1,L2:] such that A4:
for b being Element of [:L1,L2:] holds
( a "/\" b = a & b "/\" a = a )
; :: according to LATTICES:def 13 :: thesis: ( L1 is lower-bounded & L2 is lower-bounded )
consider p1 being Element of L1, p2 being Element of L2 such that
A5:
a = [p1,p2]
by DOMAIN_1:9;
thus
L1 is lower-bounded
:: thesis: L2 is lower-bounded
take
p2
; :: according to LATTICES:def 13 :: thesis: for b1 being Element of the carrier of L2 holds
( p2 "/\" b1 = p2 & b1 "/\" p2 = p2 )
let q2 be Element of L2; :: thesis: ( p2 "/\" q2 = p2 & q2 "/\" p2 = p2 )
consider q1 being Element of L1;
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