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 for x being object st x in dom Mi holds
Mi . x in Alet x be
object ;
( x in dom Mi implies Mi . x in A )assume A4:
x in dom Mi
;
Mi . x in Athen 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;
verum end;
A10:
now for x being object st x in dom Ma holds
Ma . x in Alet x be
object ;
( x in dom Ma implies Ma . x in A )assume A11:
x in dom Ma
;
Ma . x in Athen 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;
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 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;
( 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)
;
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)
;
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;
A23:
now for p, q, r being Element of L holds p "/\" (q "/\" r) = (p "/\" q) "/\" rlet p,
q,
r be
Element of
L;
p "/\" (q "/\" r) = (p "/\" q) "/\" rreconsider 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
;
verum end;
now for p, q, r being Element of L holds p "\/" (q "\/" r) = (p "\/" q) "\/" rlet p,
q,
r be
Element of
L;
p "\/" (q "\/" r) = (p "\/" q) "\/" rreconsider 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
;
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
; ( 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.] )
; verum