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 ;
A3: the L_meet of (RealSubLatt (r1,r2)) = minreal || [.r1,r2.] by ;
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
( 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 ; :: thesis: 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 ) ) :: 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 ;
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 ;
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
.= minreal . [b,a] by
.= minreal . (b,a)
.= min (b9,r2) by REAL_LAT:def 1
.= b by ;
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
( 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 ;
then reconsider X1 = X as non empty Subset of ExtREAL by ;
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 ;
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 ;
hence r1 - 1 <= v by ; :: thesis: verum
end;
then A10: X1 is bounded_below ;
X <> then A11: inf X1 in REAL by ;
the Element of X1 in [.r1,r2.] by ;
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 ;
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 ;
then reconsider a = inf X1 as Element of (RealSubLatt (r1,r2)) by ;
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 ;
a "/\" q = (minreal || [.r1,r2.]) . (a,q) by
.= minreal . [a,q] by
.= minreal . (a,q)
.= min (a9,q9) by REAL_LAT:def 1
.= a by ;
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 ;
then reconsider h9 = h as Real ;
A20: b [= h1 by ;
min (b9,h9) = minreal . (b,h1) by REAL_LAT:def 1
.= (minreal || [.r1,r2.]) . [b,h1] by
.= (minreal || [.r1,r2.]) . (b,h1)
.= b "/\" h1 by
.= b9 by ;
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
.= minreal . [b,a] by
.= minreal . (b,a)
.= min (b9,a9) by REAL_LAT:def 1
.= b by ;
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