let r be Real; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
( r = upper_bound seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) )
let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies ( r = upper_bound seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) ) )
set R = rng seq;
assume seq is bounded_above ; :: thesis: ( r = upper_bound seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) )
then A1: rng seq is bounded_above by Th5;
A2: rng seq <> {} by RELAT_1:41;
A3: ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) implies r = upper_bound seq )

proof

assume that
A4: for n being Nat holds seq . n <= r and
A5: for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ; :: thesis: r = upper_bound seq

A6: now :: thesis: for s being Real st 0 < s holds
ex r2 being Real st
( r2 in rng seq & r - s < r2 )

let s be Real; :: thesis: ( 0 < s implies ex r2 being Real st
( r2 in rng seq & r - s < r2 ) )
assume 0 < s ; :: thesis: ex r2 being Real st
( r2 in rng seq & r - s < r2 )
then consider k being Nat such that
A7: r - s < seq . k by A5;
A8: k in NAT by ORDINAL1:def 12;
consider r2 being Real such that
A9: ( r2 in rng seq & r2 = seq . k ) by FUNCT_2:4, A8;
take r2 = r2; :: thesis: ( r2 in rng seq & r - s < r2 )
thus ( r2 in rng seq & r - s < r2 ) by A7, A9; :: thesis: verum

end;

now :: thesis: for r1 being Real st r1 in rng seq holds
r1 <= r

let r1 be Real; :: thesis: ( r1 in rng seq implies r1 <= r )
assume r1 in rng seq ; :: thesis: r1 <= r
then ex n being object st
( n in dom seq & seq . n = r1 ) by FUNCT_1:def 3;
hence r1 <= r by A4; :: thesis: verum

end;

hence r = upper_bound seq by A1, A2, A6, SEQ_4:def 1; :: thesis: verum

end;

( r = upper_bound seq implies ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) )

proof

assume A10: r = upper_bound seq ; :: thesis: ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) )

A11: now :: thesis: for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k

let s be Real; :: thesis: ( 0 < s implies ex k being Nat st r - s < seq . k )
assume 0 < s ; :: thesis: ex k being Nat st r - s < seq . k
then consider r2 being Real such that
A12: r2 in rng seq and
A13: r - s < r2 by A1, A2, A10, SEQ_4:def 1;
consider k being Nat such that
A14: r2 = seq . k by A12, SETLIM_1:4;
reconsider k = k as Nat ;
take k = k; :: thesis: r - s < seq . k
thus r - s < seq . k by A13, A14; :: thesis: verum

end;

now :: thesis: for n being Nat holds seq . n <= r

let n be Nat; :: thesis: seq . n <= r
A15: n in NAT by ORDINAL1:def 12;
seq . n in rng seq by FUNCT_2:4, A15;
hence seq . n <= r by A1, A10, SEQ_4:def 1; :: thesis: verum

end;

hence ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) by A11; :: thesis: verum

end;

hence ( r = upper_bound seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) ) by A3; :: thesis: verum