let R be non empty interval RelStr ; :: thesis: for X being set holds ex_sup_of X,R
let X be set ; :: thesis: ex_sup_of X,R
consider a, b being real number such that
A1: ( a <= b & the carrier of R = [.a,b.] ) by Def2;
reconsider a = a, b = b as Real by XREAL_0:def 1;
A2: X /\ [.a,b.] c= [.a,b.] by XBOOLE_1:17;
reconsider Y = X /\ [.a,b.] as Subset of REAL ;
[.a,b.] is closed-interval by A1, INTEGRA1:def 1;
then A3: [.a,b.] is bounded_above by INTEGRA1:3;
then A4: Y is bounded_above by XBOOLE_1:17, XXREAL_2:43;
ex a being Element of R st
( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds
a <<= b ) )

proof

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

suppose A5: Y is empty ; :: thesis: ex a being Element of R st
( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds
a <<= b ) )

reconsider x = a as Element of R by A1, XXREAL_1:1;
take x ; :: thesis: ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
x <<= b ) )
thus Y is_<=_than x by A5, YELLOW_0:6; :: thesis: for b being Element of R st Y is_<=_than b holds
x <<= b
let y be Element of R; :: thesis: ( Y is_<=_than y implies x <<= y )
x <= y by A1, XXREAL_1:1;
hence ( Y is_<=_than y implies x <<= y ) by Th3; :: thesis: verum

end;

suppose A6: not Y is empty ; :: thesis: ex a being Element of R st
( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds
a <<= b ) )

upper_bound [.a,b.] = b by A1, JORDAN5A:20;
then A7: upper_bound Y <= b by A3, A6, SEQ_4:65, XBOOLE_1:17;
consider c being Element of Y;
A8: c in Y by A6;
then reconsider c = c as Real ;
A9: c <= upper_bound Y by A4, A6, SEQ_4:def 4;
a <= c by A2, A8, XXREAL_1:1;
then a <= upper_bound Y by A9, XXREAL_0:2;
then reconsider x = upper_bound Y as Element of R by A1, A7, XXREAL_1:1;
take x ; :: thesis: ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
x <<= b ) )
A10: for b being Element of R st b in Y holds
b <<= x

proof

let b be Element of R; :: thesis: ( b in Y implies b <<= x )
assume b in Y ; :: thesis: b <<= x
then b <= upper_bound Y by A4, SEQ_4:def 4;
hence b <<= x by Th3; :: thesis: verum

end;

for y being Element of R st Y is_<=_than y holds
x <<= y

proof

let y be Element of R; :: thesis: ( Y is_<=_than y implies x <<= y )
assume A11: Y is_<=_than y ; :: thesis: x <<= y
for z being real number st z in Y holds
z <= y

proof

let z be real number ; :: thesis: ( z in Y implies z <= y )
assume A12: z in Y ; :: thesis: z <= y
then reconsider z = z as Element of R by A1, XBOOLE_0:def 4;
z <<= y by A11, A12, LATTICE3:def 9;
hence z <= y by Th3; :: thesis: verum

end;

then upper_bound Y <= y by A6, TOPMETR3:1;
hence x <<= y by Th3; :: thesis: verum

end;

hence ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
x <<= b ) ) by A10, LATTICE3:def 9; :: thesis: verum

end;

end;

end;

then ex_sup_of Y,R by YELLOW_0:15;
hence ex_sup_of X,R by A1, YELLOW_0:50; :: thesis: verum