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 such that
A1: a <= b and
A2: the carrier of R = [.a,b.] by Def2;
reconsider a = a, b = b as Real ;
reconsider Y = X /\ [.a,b.] as Subset of REAL ;
( not [.a,b.] is empty & [.a,b.] is closed_interval ) by A1, MEASURE5:14;
then A3: [.a,b.] is bounded_above by INTEGRA1:3;
then A4: Y is bounded_above by XBOOLE_1:17, XXREAL_2:43;
A5: X /\ [.a,b.] c= [.a,b.] by XBOOLE_1:17;
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 A6: 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, A2, 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 A6; :: 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 A2, XXREAL_1:1;
hence ( Y is_<=_than y implies x <<= y ) by Th3; :: thesis: verum

end;

suppose A7: 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 ) )

set c = the Element of Y;
A8: the Element of Y in Y by A7;
reconsider c = the Element of Y as Real ;
A9: a <= c by A5, A8, XXREAL_1:1;
c <= upper_bound Y by A4, A7, SEQ_4:def 1;
then A10: a <= upper_bound Y by A9, XXREAL_0:2;
upper_bound [.a,b.] = b by A1, JORDAN5A:19;
then upper_bound Y <= b by A3, A7, SEQ_4:48, XBOOLE_1:17;
then reconsider x = upper_bound Y as Element of R by A2, A10, XXREAL_1:1;
A11: 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 A12: Y is_<=_than y ; :: thesis: x <<= y
for z being Real st z in Y holds
z <= y

proof

let z be Real; :: thesis: ( z in Y implies z <= y )
assume A13: z in Y ; :: thesis: z <= y
then reconsider z = z as Element of R by A2, XBOOLE_0:def 4;
z <<= y by A12, A13;
hence z <= y by Th3; :: thesis: verum

end;

then upper_bound Y <= y by A7, SEQ_4:144;
hence x <<= y by Th3; :: thesis: verum

end;

take x ; :: thesis: ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
x <<= b ) )
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 1;
hence b <<= x 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 A11; :: thesis: verum

end;

end;

end;

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