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

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

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

then
ex_sup_of Y,R
by YELLOW_0:15;per cases
( Y is empty or not Y is empty )
;

end;

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

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

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

( 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

x <<= b ) )

for b being Element of R st b in Y holds

b <<= x

x <<= b ) ) by A11; :: thesis: verum

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

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

hence x <<= y by Th3; :: thesis: verum

end;assume A12: Y is_<=_than y ; :: thesis: x <<= y

for z being Real st z in Y holds

z <= y

proof

then
upper_bound Y <= y
by A7, SEQ_4:144;
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;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

hence x <<= y by Th3; :: thesis: verum

x <<= b ) )

for b being Element of R st b in Y holds

b <<= x

proof

hence
( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds
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;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

x <<= b ) ) by A11; :: thesis: verum

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