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 ;
then A3: [.a,b.] is bounded_above by INTEGRA1:3;
then A4: Y is bounded_above by ;
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 ;
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 ;
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 ;
c <= upper_bound Y by ;
then A10: a <= upper_bound Y by ;
upper_bound [.a,b.] = b by ;
then upper_bound Y <= b by ;
then reconsider x = upper_bound Y as Element of R by ;
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 ;
z <<= y by ;
hence z <= y by Th3; :: thesis: verum
end;
then upper_bound Y <= y by ;
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 ;
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 ; :: thesis: verum