r2 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by A1;

then reconsider A = [.r1,r2.] as non empty set by RCOMP_1:def 1;

[:A,A:] c= [:REAL,REAL:] by ZFMISC_1:96;

then reconsider Ma = maxreal || A, Mi = minreal || A as Function of [:A,A:],REAL by FUNCT_2:32;

A2: dom Mi = [:A,A:] by FUNCT_2:def 1;

dom Ma = [:A,A:] by FUNCT_2:def 1;

then reconsider Ma = Ma as BinOp of A by A10, FUNCT_2:3;

set R = Real_Lattice ;

set L9 = LattStr(# A,Ma,Mi #);

reconsider L = LattStr(# A,Ma,Mi #) as non empty LattStr ;

then reconsider L9 = LattStr(# A,Ma,Mi #) as strict Lattice ;

take L9 ; :: thesis: ( the carrier of L9 = [.r1,r2.] & the L_join of L9 = maxreal || [.r1,r2.] & the L_meet of L9 = minreal || [.r1,r2.] )

thus ( the carrier of L9 = [.r1,r2.] & the L_join of L9 = maxreal || [.r1,r2.] & the L_meet of L9 = minreal || [.r1,r2.] ) ; :: thesis: verum

then reconsider A = [.r1,r2.] as non empty set by RCOMP_1:def 1;

[:A,A:] c= [:REAL,REAL:] by ZFMISC_1:96;

then reconsider Ma = maxreal || A, Mi = minreal || A as Function of [:A,A:],REAL by FUNCT_2:32;

A2: dom Mi = [:A,A:] by FUNCT_2:def 1;

A3: now :: thesis: for x being object st x in dom Mi holds

Mi . x in A

Mi . x in A

let x be object ; :: thesis: ( x in dom Mi implies Mi . x in A )

assume A4: x in dom Mi ; :: thesis: Mi . x in A

then consider x1, x2 being object such that

A5: x = [x1,x2] by RELAT_1:def 1;

x2 in A by A4, A5, ZFMISC_1:87;

then x2 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y2 being Real such that

A6: x2 = y2 and

A7: ( r1 <= y2 & y2 <= r2 ) ;

reconsider y2 = y2 as Real ;

x1 in A by A4, A5, ZFMISC_1:87;

then x1 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y1 being Real such that

A8: x1 = y1 and

A9: ( r1 <= y1 & y1 <= r2 ) ;

reconsider y1 = y1 as Real ;

Mi . x = minreal . (x1,x2) by A4, A5, FUNCT_1:49

.= min (y1,y2) by A8, A6, REAL_LAT:def 1 ;

then ( Mi . x = y1 or Mi . x = y2 ) by XXREAL_0:15;

then Mi . x in { r where r is Real : ( r1 <= r & r <= r2 ) } by A9, A7;

hence Mi . x in A by RCOMP_1:def 1; :: thesis: verum

end;assume A4: x in dom Mi ; :: thesis: Mi . x in A

then consider x1, x2 being object such that

A5: x = [x1,x2] by RELAT_1:def 1;

x2 in A by A4, A5, ZFMISC_1:87;

then x2 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y2 being Real such that

A6: x2 = y2 and

A7: ( r1 <= y2 & y2 <= r2 ) ;

reconsider y2 = y2 as Real ;

x1 in A by A4, A5, ZFMISC_1:87;

then x1 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y1 being Real such that

A8: x1 = y1 and

A9: ( r1 <= y1 & y1 <= r2 ) ;

reconsider y1 = y1 as Real ;

Mi . x = minreal . (x1,x2) by A4, A5, FUNCT_1:49

.= min (y1,y2) by A8, A6, REAL_LAT:def 1 ;

then ( Mi . x = y1 or Mi . x = y2 ) by XXREAL_0:15;

then Mi . x in { r where r is Real : ( r1 <= r & r <= r2 ) } by A9, A7;

hence Mi . x in A by RCOMP_1:def 1; :: thesis: verum

A10: now :: thesis: for x being object st x in dom Ma holds

Ma . x in A

reconsider Mi = Mi as BinOp of A by A2, A3, FUNCT_2:3;Ma . x in A

let x be object ; :: thesis: ( x in dom Ma implies Ma . x in A )

assume A11: x in dom Ma ; :: thesis: Ma . x in A

then consider x1, x2 being object such that

A12: x = [x1,x2] by RELAT_1:def 1;

x2 in A by A11, A12, ZFMISC_1:87;

then x2 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y2 being Real such that

A13: x2 = y2 and

A14: ( r1 <= y2 & y2 <= r2 ) ;

reconsider y2 = y2 as Real ;

x1 in A by A11, A12, ZFMISC_1:87;

then x1 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y1 being Real such that

A15: x1 = y1 and

A16: ( r1 <= y1 & y1 <= r2 ) ;

reconsider y1 = y1 as Real ;

Ma . x = maxreal . (x1,x2) by A11, A12, FUNCT_1:49

.= max (y1,y2) by A15, A13, REAL_LAT:def 2 ;

then ( Ma . x = y1 or Ma . x = y2 ) by XXREAL_0:16;

then Ma . x in { r where r is Real : ( r1 <= r & r <= r2 ) } by A16, A14;

hence Ma . x in A by RCOMP_1:def 1; :: thesis: verum

end;assume A11: x in dom Ma ; :: thesis: Ma . x in A

then consider x1, x2 being object such that

A12: x = [x1,x2] by RELAT_1:def 1;

x2 in A by A11, A12, ZFMISC_1:87;

then x2 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y2 being Real such that

A13: x2 = y2 and

A14: ( r1 <= y2 & y2 <= r2 ) ;

reconsider y2 = y2 as Real ;

x1 in A by A11, A12, ZFMISC_1:87;

then x1 in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;

then consider y1 being Real such that

A15: x1 = y1 and

A16: ( r1 <= y1 & y1 <= r2 ) ;

reconsider y1 = y1 as Real ;

Ma . x = maxreal . (x1,x2) by A11, A12, FUNCT_1:49

.= max (y1,y2) by A15, A13, REAL_LAT:def 2 ;

then ( Ma . x = y1 or Ma . x = y2 ) by XXREAL_0:16;

then Ma . x in { r where r is Real : ( r1 <= r & r <= r2 ) } by A16, A14;

hence Ma . x in A by RCOMP_1:def 1; :: thesis: verum

dom Ma = [:A,A:] by FUNCT_2:def 1;

then reconsider Ma = Ma as BinOp of A by A10, FUNCT_2:3;

set R = Real_Lattice ;

set L9 = LattStr(# A,Ma,Mi #);

reconsider L = LattStr(# A,Ma,Mi #) as non empty LattStr ;

A17: now :: thesis: for a, b being Element of L holds

( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )

A18:
for x being Element of A holds x is Element of Real_Lattice
by REAL_LAT:def 3, XREAL_0:def 1;( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )

let a, b be Element of L; :: thesis: ( a "\/" b = maxreal . (a,b) & a "/\" b = minreal . (a,b) )

thus a "\/" b = the L_join of L . (a,b) by LATTICES:def 1

.= maxreal . [a,b] by FUNCT_1:49

.= maxreal . (a,b) ; :: thesis: a "/\" b = minreal . (a,b)

thus a "/\" b = the L_meet of L . (a,b) by LATTICES:def 2

.= minreal . [a,b] by FUNCT_1:49

.= minreal . (a,b) ; :: thesis: verum

end;thus a "\/" b = the L_join of L . (a,b) by LATTICES:def 1

.= maxreal . [a,b] by FUNCT_1:49

.= maxreal . (a,b) ; :: thesis: a "/\" b = minreal . (a,b)

thus a "/\" b = the L_meet of L . (a,b) by LATTICES:def 2

.= minreal . [a,b] by FUNCT_1:49

.= minreal . (a,b) ; :: thesis: verum

A19: now :: thesis: for p, q being Element of L holds p "\/" q = q "\/" p

let p, q be Element of L; :: thesis: p "\/" q = q "\/" p

reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus p "\/" q = maxreal . (p,q) by A17

.= maxreal . (q9,p9) by REAL_LAT:1

.= q "\/" p by A17 ; :: thesis: verum

end;reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus p "\/" q = maxreal . (p,q) by A17

.= maxreal . (q9,p9) by REAL_LAT:1

.= q "\/" p by A17 ; :: thesis: verum

A20: now :: thesis: for p, q being Element of L holds p "/\" (p "\/" q) = p

let p, q be Element of L; :: thesis: p "/\" (p "\/" q) = p

reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus p "/\" (p "\/" q) = minreal . (p,(p "\/" q)) by A17

.= minreal . (p9,(maxreal . (p9,q9))) by A17

.= p by REAL_LAT:6 ; :: thesis: verum

end;reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus p "/\" (p "\/" q) = minreal . (p,(p "\/" q)) by A17

.= minreal . (p9,(maxreal . (p9,q9))) by A17

.= p by REAL_LAT:6 ; :: thesis: verum

A21: now :: thesis: for p, q being Element of L holds p "/\" q = q "/\" p

let p, q be Element of L; :: thesis: p "/\" q = q "/\" p

reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus p "/\" q = minreal . (p,q) by A17

.= minreal . (q9,p9) by REAL_LAT:2

.= q "/\" p by A17 ; :: thesis: verum

end;reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus p "/\" q = minreal . (p,q) by A17

.= minreal . (q9,p9) by REAL_LAT:2

.= q "/\" p by A17 ; :: thesis: verum

A22: now :: thesis: for p, q being Element of L holds (p "/\" q) "\/" q = q

let p, q be Element of L; :: thesis: (p "/\" q) "\/" q = q

reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus (p "/\" q) "\/" q = maxreal . ((p "/\" q),q) by A17

.= maxreal . ((minreal . (p9,q9)),q9) by A17

.= q by REAL_LAT:5 ; :: thesis: verum

end;reconsider p9 = p, q9 = q as Element of Real_Lattice by A18;

thus (p "/\" q) "\/" q = maxreal . ((p "/\" q),q) by A17

.= maxreal . ((minreal . (p9,q9)),q9) by A17

.= q by REAL_LAT:5 ; :: thesis: verum

A23: now :: thesis: for p, q, r being Element of L holds p "/\" (q "/\" r) = (p "/\" q) "/\" r

let p, q, r be Element of L; :: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r

reconsider p9 = p, q9 = q, r9 = r as Element of Real_Lattice by A18;

thus p "/\" (q "/\" r) = minreal . (p,(q "/\" r)) by A17

.= minreal . (p,(minreal . (q,r))) by A17

.= minreal . ((minreal . (p9,q9)),r9) by REAL_LAT:4

.= minreal . ((p "/\" q),r) by A17

.= (p "/\" q) "/\" r by A17 ; :: thesis: verum

end;reconsider p9 = p, q9 = q, r9 = r as Element of Real_Lattice by A18;

thus p "/\" (q "/\" r) = minreal . (p,(q "/\" r)) by A17

.= minreal . (p,(minreal . (q,r))) by A17

.= minreal . ((minreal . (p9,q9)),r9) by REAL_LAT:4

.= minreal . ((p "/\" q),r) by A17

.= (p "/\" q) "/\" r by A17 ; :: thesis: verum

now :: thesis: for p, q, r being Element of L holds p "\/" (q "\/" r) = (p "\/" q) "\/" r

then
( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
by A19, A22, A21, A23, A20, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;let p, q, r be Element of L; :: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r

reconsider p9 = p, q9 = q, r9 = r as Element of Real_Lattice by A18;

thus p "\/" (q "\/" r) = maxreal . (p,(q "\/" r)) by A17

.= maxreal . (p,(maxreal . (q,r))) by A17

.= maxreal . ((maxreal . (p9,q9)),r9) by REAL_LAT:3

.= maxreal . ((p "\/" q),r) by A17

.= (p "\/" q) "\/" r by A17 ; :: thesis: verum

end;reconsider p9 = p, q9 = q, r9 = r as Element of Real_Lattice by A18;

thus p "\/" (q "\/" r) = maxreal . (p,(q "\/" r)) by A17

.= maxreal . (p,(maxreal . (q,r))) by A17

.= maxreal . ((maxreal . (p9,q9)),r9) by REAL_LAT:3

.= maxreal . ((p "\/" q),r) by A17

.= (p "\/" q) "\/" r by A17 ; :: thesis: verum

then reconsider L9 = LattStr(# A,Ma,Mi #) as strict Lattice ;

take L9 ; :: thesis: ( the carrier of L9 = [.r1,r2.] & the L_join of L9 = maxreal || [.r1,r2.] & the L_meet of L9 = minreal || [.r1,r2.] )

thus ( the carrier of L9 = [.r1,r2.] & the L_join of L9 = maxreal || [.r1,r2.] & the L_meet of L9 = minreal || [.r1,r2.] ) ; :: thesis: verum