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;

A3: now :: thesis: for x being object st x in dom Mi holds
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;

A10: now :: thesis: for x being object st x in dom Ma holds
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;

reconsider Mi = Mi as BinOp of A by A2, A3, FUNCT_2:3;
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) )

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;

A18: for x being Element of A holds x is Element of Real_Lattice by REAL_LAT:def 3, XREAL_0:def 1;

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;

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;

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;

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;

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;

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

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