let r1, r2 be Real; ( r1 <= r2 implies RealSubLatt (r1,r2) is complete )
assume A1:
r1 <= r2
; RealSubLatt (r1,r2) is complete
reconsider R1 = r1, R2 = r2 as R_eal by XXREAL_0:def 1;
set A = [.r1,r2.];
set L9 = RealSubLatt (r1,r2);
A2:
the carrier of (RealSubLatt (r1,r2)) = [.r1,r2.]
by A1, Def4;
A3:
the L_meet of (RealSubLatt (r1,r2)) = minreal || [.r1,r2.]
by A1, Def4;
now for X being Subset of (RealSubLatt (r1,r2)) ex a being Element of (RealSubLatt (r1,r2)) st
( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a ) )let X be
Subset of
(RealSubLatt (r1,r2));
ex a being Element of (RealSubLatt (r1,r2)) st
( b2 is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b3 is_less_than a holds
b3 [= b ) )per cases
( X is empty or not X is empty )
;
suppose A4:
X is
empty
;
ex a being Element of (RealSubLatt (r1,r2)) st
( b2 is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b3 is_less_than a holds
b3 [= b ) )thus
ex
a being
Element of
(RealSubLatt (r1,r2)) st
(
a is_less_than X & ( for
b being
Element of
(RealSubLatt (r1,r2)) st
b is_less_than X holds
b [= a ) )
verumproof
r2 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by A1;
then reconsider a =
r2 as
Element of
(RealSubLatt (r1,r2)) by A2, RCOMP_1:def 1;
take
a
;
( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a ) )
for
q being
Element of
(RealSubLatt (r1,r2)) st
q in X holds
a [= q
by A4;
hence
a is_less_than X
;
for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a
let b be
Element of
(RealSubLatt (r1,r2));
( b is_less_than X implies b [= a )
assume
b is_less_than X
;
b [= a
A5:
b in [.r1,r2.]
by A2;
then reconsider b9 =
b as
Element of
REAL ;
b in { r where r is Real : ( r1 <= r & r <= r2 ) }
by A5, RCOMP_1:def 1;
then consider b1 being
Real such that A6:
(
b = b1 &
r1 <= b1 &
b1 <= r2 )
;
reconsider b1 =
b1,
r2 =
r2 as
Real ;
b "/\" a =
(minreal || [.r1,r2.]) . (
b,
a)
by A3, LATTICES:def 2
.=
minreal . [b,a]
by A2, FUNCT_1:49
.=
minreal . (
b,
a)
.=
min (
b9,
r2)
by REAL_LAT:def 1
.=
b
by A6, XXREAL_0:def 9
;
hence
b [= a
by LATTICES:4;
verum
end; end; suppose A7:
not
X is
empty
;
ex a being Element of (RealSubLatt (r1,r2)) st
( b2 is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b3 is_less_than a holds
b3 [= b ) )
X c= REAL
by A2, XBOOLE_1:1;
then reconsider X1 =
X as non
empty Subset of
ExtREAL by A7, NUMBERS:31, XBOOLE_1:1;
thus
ex
a being
Element of
(RealSubLatt (r1,r2)) st
(
a is_less_than X & ( for
b being
Element of
(RealSubLatt (r1,r2)) st
b is_less_than X holds
b [= a ) )
verumproof
set g = the
Element of
X1;
set A1 =
inf X1;
set LB =
r1 - 1;
r1 - 1 is
LowerBound of
X1
then A10:
X1 is
bounded_below
;
X <> {+infty}
then A11:
inf X1 in REAL
by A10, XXREAL_2:58;
the
Element of
X1 in [.r1,r2.]
by A2, TARSKI:def 3;
then
the
Element of
X1 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by RCOMP_1:def 1;
then A12:
ex
w being
Real st
( the
Element of
X1 = w &
r1 <= w &
w <= r2 )
;
A13:
inf X1 is
LowerBound of
X1
by XXREAL_2:def 4;
then
inf X1 <= the
Element of
X1
by XXREAL_2:def 2;
then consider A9,
R29 being
Real such that A14:
A9 = inf X1
and A15:
(
R29 = R2 &
A9 <= R29 )
by A11, A12, XXREAL_0:2;
then
R1 is
LowerBound of
X1
by XXREAL_2:def 2;
then
R1 <= inf X1
by XXREAL_2:def 4;
then
A9 in { r where r is Real : ( r1 <= r & r <= r2 ) }
by A14, A15;
then reconsider a =
inf X1 as
Element of
(RealSubLatt (r1,r2)) by A2, A14, RCOMP_1:def 1;
take
a
;
( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a ) )
a in [.r1,r2.]
by A2;
then reconsider a9 =
a as
Element of
REAL ;
now for q being Element of (RealSubLatt (r1,r2)) st q in X holds
a [= qlet q be
Element of
(RealSubLatt (r1,r2));
( q in X implies a [= q )assume A16:
q in X
;
a [= q
q in [.r1,r2.]
by A2;
then reconsider q9 =
q as
Element of
REAL ;
reconsider Q =
q9 as
R_eal by NUMBERS:31;
inf X1 = a9
;
then A17:
ex
a1,
q1 being
Real st
(
a1 = inf X1 &
q1 = Q &
a1 <= q1 )
by A13, A16, XXREAL_2:def 2;
a "/\" q =
(minreal || [.r1,r2.]) . (
a,
q)
by A3, LATTICES:def 2
.=
minreal . [a,q]
by A2, FUNCT_1:49
.=
minreal . (
a,
q)
.=
min (
a9,
q9)
by REAL_LAT:def 1
.=
a
by A17, XXREAL_0:def 9
;
hence
a [= q
by LATTICES:4;
verum end;
hence
a is_less_than X
;
for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds
b [= a
let b be
Element of
(RealSubLatt (r1,r2));
( b is_less_than X implies b [= a )
b in [.r1,r2.]
by A2;
then reconsider b9 =
b as
Element of
REAL ;
reconsider B =
b9 as
R_eal by NUMBERS:31;
assume A18:
b is_less_than X
;
b [= a
now for h being ExtReal st h in X holds
B <= hlet h be
ExtReal;
( h in X implies B <= h )assume A19:
h in X
;
B <= hthen reconsider h1 =
h as
Element of
(RealSubLatt (r1,r2)) ;
h in [.r1,r2.]
by A2, A19;
then reconsider h9 =
h as
Real ;
A20:
b [= h1
by A18, A19;
min (
b9,
h9) =
minreal . (
b,
h1)
by REAL_LAT:def 1
.=
(minreal || [.r1,r2.]) . [b,h1]
by A2, FUNCT_1:49
.=
(minreal || [.r1,r2.]) . (
b,
h1)
.=
b "/\" h1
by A3, LATTICES:def 2
.=
b9
by A20, LATTICES:4
;
hence
B <= h
by XXREAL_0:def 9;
verum end;
then
B is
LowerBound of
X1
by XXREAL_2:def 2;
then A21:
B <= inf X1
by XXREAL_2:def 4;
b "/\" a =
(minreal || [.r1,r2.]) . (
b,
a)
by A3, LATTICES:def 2
.=
minreal . [b,a]
by A2, FUNCT_1:49
.=
minreal . (
b,
a)
.=
min (
b9,
a9)
by REAL_LAT:def 1
.=
b
by A21, XXREAL_0:def 9
;
hence
b [= a
by LATTICES:4;
verum
end; end; end; end;
hence
RealSubLatt (r1,r2) is complete
by VECTSP_8:def 6; verum