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

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:

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 A4;
hence a is_less_than X ; :: thesis:
let b be Element of (RealSubLatt (r1,r2)); :: thesis:
assume b is_less_than X ; :: thesis:
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:

end;

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:

set g = the Element of X1;
set A1 = inf X1;
set LB = r1 - 1;
r1 - 1 is LowerBound of X1

let v be ExtReal; :: according to XXREAL_2:def 2 :: 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 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:

end;

end;

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;

let v be ExtReal; :: 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 ex w being Real st
( v = w & r1 <= w & w <= r2 ) ;
hence R1 <= v ; :: thesis:

end;

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 ; :: thesis:
a in [.r1,r2.] by A2;
then reconsider a9 = a as Element of REAL ;

let q be Element of (RealSubLatt (r1,r2)); :: thesis:
assume A16: q in X ; :: thesis:
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:

end;

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

let h be ExtReal; :: 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 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:

end;

end;