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 ) )

( 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:1;

thus L1 is lower-bounded :: thesis: L2 is lower-bounded

take p2 ; :: according to LATTICES:def 13 :: thesis: for b_{1} being Element of the carrier of L2 holds

( p2 "/\" b_{1} = p2 & b_{1} "/\" p2 = p2 )

let q2 be Element of L2; :: thesis: ( 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; :: thesis: verum

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 a being Element of [:L1,L2:] such that A4:
for b being Element of [:L1,L2:] holds
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 b_{1} being Element of the carrier of [:L1,L2:] holds

( a "/\" b_{1} = a & b_{1} "/\" 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:1;

thus a "/\" b = [(p1 "/\" q1),(p2 "/\" q2)] by A3, Th21

.= [p1,(p2 "/\" q2)] by A1

.= a by A2 ; :: thesis: b "/\" a = a

hence b "/\" a = a ; :: thesis: verum

end;( 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 b

( a "/\" b

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:1;

thus a "/\" b = [(p1 "/\" q1),(p2 "/\" q2)] by A3, Th21

.= [p1,(p2 "/\" q2)] by A1

.= a by A2 ; :: thesis: b "/\" a = a

hence b "/\" a = a ; :: thesis: verum

( 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:1;

thus L1 is lower-bounded :: thesis: L2 is lower-bounded

proof

set q1 = the Element of L1;
set q2 = the Element of L2;

take p1 ; :: according to LATTICES:def 13 :: thesis: for b_{1} being Element of the carrier of L1 holds

( p1 "/\" b_{1} = p1 & b_{1} "/\" p1 = p1 )

let q1 be Element of L1; :: thesis: ( p1 "/\" q1 = p1 & q1 "/\" p1 = p1 )

a = a "/\" [q1, the Element of L2] by A4

.= [(p1 "/\" q1),(p2 "/\" the Element of L2)] by A5, Th21 ;

hence ( p1 "/\" q1 = p1 & q1 "/\" p1 = p1 ) by A5, XTUPLE_0:1; :: thesis: verum

end;take p1 ; :: according to LATTICES:def 13 :: thesis: for b

( p1 "/\" b

let q1 be Element of L1; :: thesis: ( p1 "/\" q1 = p1 & q1 "/\" p1 = p1 )

a = a "/\" [q1, the Element of L2] by A4

.= [(p1 "/\" q1),(p2 "/\" the Element of L2)] by A5, Th21 ;

hence ( p1 "/\" q1 = p1 & q1 "/\" p1 = p1 ) by A5, XTUPLE_0:1; :: thesis: verum

take p2 ; :: according to LATTICES:def 13 :: thesis: for b

( p2 "/\" b

let q2 be Element of L2; :: thesis: ( 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; :: thesis: verum