let r1, r2 be Real; :: thesis:
assume A1: r1 <= r2 ; :: thesis:
set A = [.r1,r2.];
set L' = RealSubLatt r1,r2;
reconsider R1 = r1, R2 = r2 as R_eal by XXREAL_0:def 1;
A2: ( the carrier of (RealSubLatt r1,r2) = [.r1,r2.] & the L_join of (RealSubLatt r1,r2) = maxreal || [.r1,r2.] & the L_meet of (RealSubLatt r1,r2) = minreal || [.r1,r2.] ) by A1, Def4;

now

let X be Subset of (RealSubLatt r1,r2); :: thesis:

per cases ;

suppose A3: X is empty ; :: thesis:

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:

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:
for q being Element of (RealSubLatt r1,r2) st q in X holds
a [= q by A3;
hence a is_less_than X by LATTICE3:def 16; :: thesis:
let b be Element of (RealSubLatt r1,r2); :: thesis:
A4: b in [.r1,r2.] by A2;
then b in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;
then consider b1 being Element of REAL such that
A5: ( b = b1 & r1 <= b1 & b1 <= r2 ) ;
reconsider b' = b as Element of REAL by A4;
assume b is_less_than X ; :: thesis:
b "/\" a = (minreal || [.r1,r2.]) . b,a by A2, LATTICES:def 2
.= minreal . [b,a] by A2, FUNCT_1:72
.= minreal . b,a
.= min b',r2 by REAL_LAT:def 1
.= b by A5, XXREAL_0:def 9 ;
hence b [= a by LATTICES:21; :: thesis:

end;

suppose A6: not X is empty ; :: thesis:

X c= REAL by A2, XBOOLE_1:1;
then reconsider X1 = X as non empty Subset of ExtREAL by A6, 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:

proof

set A1 = inf X1;
A7: ( inf X1 is LowerBound of X1 & ( for y being R_eal st y is LowerBound of X1 holds
y <= inf X1 ) ) by XXREAL_2:def 4;
ex LB being LowerBound of X1 st LB in REAL

proof

reconsider LB = r1 - 1 as R_eal by XXREAL_0:def 1;

now

let v be ext-real number ; :: thesis:
assume v in X1 ; :: thesis:
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 Element of REAL such that
A8: ( v = w & r1 <= w & w <= r2 ) ;
r1 - 1 <= r1 - 0 by XREAL_1:15;
then (r1 - 1) + r1 <= r1 + w by A8, XREAL_1:9;
hence LB <= v by A8, XREAL_1:8; :: thesis:

end;

then reconsider LB = LB as LowerBound of X1 by XXREAL_2:def 2;
take LB ; :: thesis:
thus LB in REAL ; :: thesis:

end;

then A9: X1 is bounded_below by SUPINF_1:def 12;
X <> {+infty }

proof

A10: X c= REAL by A2, XBOOLE_1:1;
assume X = {+infty } ; :: thesis:
then +infty in X by TARSKI:def 1;
hence contradiction by A10; :: thesis:

end;

then A11: inf X1 is Real by A9, XXREAL_2:58;

now

let v be ext-real number ; :: thesis:
assume v in X1 ; :: thesis:
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 consider w being Element of REAL such that
A12: ( v = w & r1 <= w & w <= r2 ) ;
thus R1 <= v by A12; :: thesis:

end;

then R1 is LowerBound of X1 by XXREAL_2:def 2;
then R1 <= inf X1 by XXREAL_2:def 4;
then consider R1', A1' being Real such that
A13: ( R1' = R1 & A1' = inf X1 & R1' <= A1' ) by A11;
consider g being Element of X1;
g in [.r1,r2.] by A2, TARSKI:def 3;
then g in { r where r is Real : ( r1 <= r & r <= r2 ) } by RCOMP_1:def 1;
then consider w being Element of REAL such that
A14: ( g = w & r1 <= w & w <= r2 ) ;
inf X1 <= g by A7, XXREAL_2:def 2;
then consider A', R2' being Real such that
A15: ( A' = inf X1 & R2' = R2 & A' <= R2' ) by A11, A14, XXREAL_0:2;
A' in { r where r is Real : ( r1 <= r & r <= r2 ) } by A13, A15;
then reconsider a = inf X1 as Element of (RealSubLatt r1,r2) by A2, A15, RCOMP_1:def 1;
a in [.r1,r2.] by A2;
then reconsider a' = a as Element of REAL ;
take a ; :: thesis:

now

let q be Element of (RealSubLatt r1,r2); :: thesis:
q in [.r1,r2.] by A2;
then reconsider q' = q as Element of REAL ;
q' in REAL ;
then reconsider Q = q' as R_eal by NUMBERS:31;
A16: inf X1 = a' ;
assume q in X ; :: thesis:
then inf X1 <= Q by A7, XXREAL_2:def 2;
then consider a1, q1 being Real such that
A17: ( a1 = inf X1 & q1 = Q & a1 <= q1 ) by A16;
a "/\" q = (minreal || [.r1,r2.]) . a,q by A2, LATTICES:def 2
.= minreal . [a,q] by A2, FUNCT_1:72
.= minreal . a,q
.= min a',q' by REAL_LAT:def 1
.= a by A17, XXREAL_0:def 9 ;
hence a [= q by LATTICES:21; :: thesis:

end;

hence a is_less_than X by LATTICE3:def 16; :: thesis:
let b be Element of (RealSubLatt r1,r2); :: thesis:
b in [.r1,r2.] by A2;
then reconsider b' = b as Element of REAL ;
b' in REAL ;
then reconsider B = b' as R_eal by NUMBERS:31;
assume A18: b is_less_than X ; :: thesis:

now

let h be ext-real number ; :: thesis:
assume A19: h in X ; :: thesis:
then reconsider h1 = h as Element of (RealSubLatt r1,r2) ;
h in [.r1,r2.] by A2, A19;
then reconsider h' = h as Real ;
A20: b [= h1 by A18, A19, LATTICE3:def 16;
min b',h' = minreal . b,h1 by REAL_LAT:def 1
.= (minreal || [.r1,r2.]) . [b,h1] by A2, FUNCT_1:72
.= (minreal || [.r1,r2.]) . b,h1
.= b "/\" h1 by A2, LATTICES:def 2
.= b' by A20, LATTICES:21 ;
hence B <= h by XXREAL_0:def 9; :: thesis:

end;

then B is LowerBound of X1 by XXREAL_2:def 2;
then B <= inf X1 by XXREAL_2:def 4;
then consider b1, a1 being Real such that
A21: ( b1 = B & a1 = inf X1 & b1 <= a1 ) by A11;
b "/\" a = (minreal || [.r1,r2.]) . b,a by A2, LATTICES:def 2
.= minreal . [b,a] by A2, FUNCT_1:72
.= minreal . b,a
.= min b',a' by REAL_LAT:def 1
.= b by A21, XXREAL_0:def 9 ;
hence b [= a by LATTICES:21; :: thesis:

end;

hence RealSubLatt r1,r2 is complete by VECTSP_8:def 6; :: thesis: