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;

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 ) )

let X be Subset of (RealSubLatt (r1,r2)); :: thesis: ex a being Element of (RealSubLatt (r1,r2)) st
( b₂ is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b₃ is_less_than a holds
b₃ [= b ) )

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

suppose A4: X is empty ; :: thesis: ex a being Element of (RealSubLatt (r1,r2)) st
( b₂ is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b₃ is_less_than a holds
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

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;

end;

suppose A7: not X is empty ; :: thesis: ex a being Element of (RealSubLatt (r1,r2)) st
( b₂ is_less_than a & ( for b being Element of (RealSubLatt (r1,r2)) st b₃ is_less_than a holds
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

proof

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

proof

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;

then A10: X1 is bounded_below ;
X <> {+infty}

proof

assume X = {+infty} ; :: thesis: contradiction
then +infty in X by TARSKI:def 1;
hence contradiction by A2; :: thesis: verum

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;

now :: thesis: for v being ExtReal st v in X1 holds
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;

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 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

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;

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 )
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

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;

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

end;

end;

end;

end;

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