let r1, r2 be Real; :: thesis: ( r1 <= r2 implies RealSubLatt (r1,r2) is complete )

assume A1: r1 <= r2 ; :: thesis: 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;

assume A1: r1 <= r2 ; :: thesis: 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 :: thesis: 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 ) )

hence
RealSubLatt (r1,r2) is complete
by VECTSP_8:def 6; :: thesis: verum( 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)); :: thesis: ex a being Element of (RealSubLatt (r1,r2)) st

( b_{2} is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b_{3} is_less_than a holds

b_{3} [= b ) )

end;( b

b

per cases
( X is empty or not X is empty )
;

end;

suppose A4:
X is empty
; :: thesis: ex a being Element of (RealSubLatt (r1,r2)) st

( b_{2} is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b_{3} is_less_than a holds

b_{3} [= b ) )

( b

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 ) ) :: thesis: verum

end;( a is_less_than X & ( for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds

b [= a ) ) :: thesis: verum

proof

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 ; :: thesis: ( 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 ; :: thesis: 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)); :: thesis: ( b is_less_than X implies b [= a )

assume b is_less_than X ; :: thesis: 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; :: thesis: verum

end;then reconsider a = r2 as Element of (RealSubLatt (r1,r2)) by A2, RCOMP_1:def 1;

take a ; :: thesis: ( 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 ; :: thesis: 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)); :: thesis: ( b is_less_than X implies b [= a )

assume b is_less_than X ; :: thesis: 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; :: thesis: verum

suppose A7:
not X is empty
; :: thesis: ex a being Element of (RealSubLatt (r1,r2)) st

( b_{2} is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b_{3} is_less_than a holds

b_{3} [= b ) )

( b

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 ) ) :: thesis: verum

end;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 ) ) :: thesis: verum

proof

set g = the Element of X1;

set A1 = inf X1;

set LB = r1 - 1;

r1 - 1 is LowerBound of X1

X <> {+infty}

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 <= 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 ; :: thesis: ( 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 ;

b [= a

let b be Element of (RealSubLatt (r1,r2)); :: thesis: ( 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 ; :: thesis: b [= a

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; :: thesis: verum

end;set A1 = inf X1;

set LB = r1 - 1;

r1 - 1 is LowerBound of X1

proof

then A10:
X1 is bounded_below
;
let v be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not v in X1 or r1 - 1 <= v )

assume v in X1 ; :: thesis: r1 - 1 <= v

then v in the carrier of (RealSubLatt (r1,r2)) ;

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

then consider w being Real such that

A8: v = w and

A9: r1 <= w and

w <= r2 ;

r1 - 1 <= r1 - 0 by XREAL_1:13;

then (r1 - 1) + r1 <= r1 + w by A9, XREAL_1:7;

hence r1 - 1 <= v by A8, XREAL_1:6; :: thesis: verum

end;assume v in X1 ; :: thesis: r1 - 1 <= v

then v in the carrier of (RealSubLatt (r1,r2)) ;

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

then consider w being Real such that

A8: v = w and

A9: r1 <= w and

w <= r2 ;

r1 - 1 <= r1 - 0 by XREAL_1:13;

then (r1 - 1) + r1 <= r1 + w by A9, XREAL_1:7;

hence r1 - 1 <= v by A8, XREAL_1:6; :: thesis: verum

X <> {+infty}

proof

then A11:
inf X1 in REAL
by A10, XXREAL_2:58;
assume
X = {+infty}
; :: thesis: contradiction

then +infty in X by TARSKI:def 1;

hence contradiction by A2; :: thesis: verum

end;then +infty in X by TARSKI:def 1;

hence contradiction by A2; :: thesis: verum

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;

now :: thesis: for v being ExtReal st v in X1 holds

R1 <= v

then
R1 is LowerBound of X1
by XXREAL_2:def 2;R1 <= v

let v be ExtReal; :: thesis: ( v in X1 implies R1 <= v )

assume v in X1 ; :: thesis: R1 <= v

then v in [.r1,r2.] by A2;

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

then ex w being Real st

( v = w & r1 <= w & w <= r2 ) ;

hence R1 <= v ; :: thesis: verum

end;assume v in X1 ; :: thesis: R1 <= v

then v in [.r1,r2.] by A2;

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

then ex w being Real st

( v = w & r1 <= w & w <= r2 ) ;

hence R1 <= v ; :: thesis: verum

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 ; :: thesis: ( 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 :: thesis: for q being Element of (RealSubLatt (r1,r2)) st q in X holds

a [= q

hence
a is_less_than X
; :: thesis: for b being Element of (RealSubLatt (r1,r2)) st b is_less_than X holds a [= q

let q be Element of (RealSubLatt (r1,r2)); :: thesis: ( q in X implies a [= q )

assume A16: q in X ; :: thesis: 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; :: thesis: verum

end;assume A16: q in X ; :: thesis: 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; :: thesis: verum

b [= a

let b be Element of (RealSubLatt (r1,r2)); :: thesis: ( 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 ; :: thesis: b [= a

now :: thesis: for h being ExtReal st h in X holds

B <= h

then
B is LowerBound of X1
by XXREAL_2:def 2;B <= h

let h be ExtReal; :: thesis: ( h in X implies B <= h )

assume A19: h in X ; :: thesis: B <= h

then 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; :: thesis: verum

end;assume A19: h in X ; :: thesis: B <= h

then 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; :: thesis: verum

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; :: thesis: verum