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:119;
then reconsider Ma = maxreal || A, Mi = minreal || A as Function of [:A,A:],REAL by FUNCT_2:38;
A2:
( dom Ma = [:A,A:] & dom Mi = [:A,A:] )
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in dom Ma implies Ma . x in A )assume A3:
x in dom Ma
;
:: thesis: Ma . x in Athen consider x1,
x2 being
set such that A4:
x = [x1,x2]
by RELAT_1:def 1;
A5:
(
x1 in A &
x2 in A )
by A3, A4, ZFMISC_1:106;
then
x1 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by RCOMP_1:def 1;
then consider y1 being
Element of
REAL such that A6:
(
x1 = y1 &
r1 <= y1 &
y1 <= r2 )
;
x2 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by A5, RCOMP_1:def 1;
then consider y2 being
Element of
REAL such that A7:
(
x2 = y2 &
r1 <= y2 &
y2 <= r2 )
;
Ma . x =
maxreal . x1,
x2
by A3, A4, FUNCT_1:72
.=
max y1,
y2
by A6, A7, 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 A6, A7;
hence
Ma . x in A
by RCOMP_1:def 1;
:: thesis: verum end;
then reconsider Ma = Ma as BinOp of A by A2, FUNCT_2:5;
now let x be
set ;
:: thesis: ( x in dom Mi implies Mi . x in A )assume A8:
x in dom Mi
;
:: thesis: Mi . x in Athen consider x1,
x2 being
set such that A9:
x = [x1,x2]
by RELAT_1:def 1;
A10:
(
x1 in A &
x2 in A )
by A8, A9, ZFMISC_1:106;
then
x1 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by RCOMP_1:def 1;
then consider y1 being
Element of
REAL such that A11:
(
x1 = y1 &
r1 <= y1 &
y1 <= r2 )
;
x2 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by A10, RCOMP_1:def 1;
then consider y2 being
Element of
REAL such that A12:
(
x2 = y2 &
r1 <= y2 &
y2 <= r2 )
;
Mi . x =
minreal . x1,
x2
by A8, A9, FUNCT_1:72
.=
min y1,
y2
by A11, A12, 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 A11, A12;
hence
Mi . x in A
by RCOMP_1:def 1;
:: thesis: verum end;
then reconsider Mi = Mi as BinOp of A by A2, FUNCT_2:5;
set R = Real_Lattice ;
set L' = LattStr(# A,Ma,Mi #);
reconsider L = LattStr(# A,Ma,Mi #) as non empty LattStr ;
A15:
now 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:72
.=
maxreal . a,
b
;
:: thesis: a "/\" b = minreal . a,bthus a "/\" b =
the
L_meet of
L . a,
b
by LATTICES:def 2
.=
minreal . [a,b]
by FUNCT_1:72
.=
minreal . a,
b
;
:: thesis: verum end;
A17:
now let p,
q,
r be
Element of
L;
:: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" rreconsider p' =
p,
q' =
q,
r' =
r as
Element of
Real_Lattice by A13;
thus p "\/" (q "\/" r) =
maxreal . p,
(q "\/" r)
by A15
.=
maxreal . p,
(maxreal . q,r)
by A15
.=
maxreal . (maxreal . p',q'),
r'
by REAL_LAT:10
.=
maxreal . (p "\/" q),
r
by A15
.=
(p "\/" q) "\/" r
by A15
;
:: thesis: verum end;
A20:
now let p,
q,
r be
Element of
L;
:: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" rreconsider p' =
p,
q' =
q,
r' =
r as
Element of
Real_Lattice by A13;
thus p "/\" (q "/\" r) =
minreal . p,
(q "/\" r)
by A15
.=
minreal . p,
(minreal . q,r)
by A15
.=
minreal . (minreal . p',q'),
r'
by REAL_LAT:11
.=
minreal . (p "/\" q),
r
by A15
.=
(p "/\" q) "/\" r
by A15
;
:: 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 A16, A17, A18, A19, A20, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
then reconsider L' = LattStr(# A,Ma,Mi #) as strict Lattice ;
take
L'
; :: thesis: ( the carrier of L' = [.r1,r2.] & the L_join of L' = maxreal || [.r1,r2.] & the L_meet of L' = minreal || [.r1,r2.] )
thus
( the carrier of L' = [.r1,r2.] & the L_join of L' = maxreal || [.r1,r2.] & the L_meet of L' = minreal || [.r1,r2.] )
; :: thesis: verum