let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
( r = sup seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )
let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies ( r = sup seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) ) )
assume seq is bounded_above ; :: thesis: ( r = sup seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )
then A1: ( rng seq is bounded_above & rng seq <> {} ) by Th5, RELAT_1:64;
set R = rng seq;
A2: ( r = sup seq implies ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )

proof

assume A3: r = sup seq ; :: thesis: ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) )

A4: now

let n be Element of NAT ; :: thesis: seq . n <= r
seq . n in rng seq by FUNCT_2:6;
hence seq . n <= r by A1, A3, SEQ_4:def 4; :: thesis: verum

end;

now

let s be real number ; :: thesis: ( 0 < s implies ex k being Element of NAT st r - s < seq . k )
assume 0 < s ; :: thesis: ex k being Element of NAT st r - s < seq . k
then consider r2 being real number such that
A5: ( r2 in rng seq & r - s < r2 ) by A1, A3, SEQ_4:def 4;
consider k being Element of NAT such that
A6: r2 = seq . k by A5, SETLIM_1:4;
take k = k; :: thesis: r - s < seq . k
thus r - s < seq . k by A5, A6; :: thesis: verum

end;

hence ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) by A4; :: thesis: verum

end;

( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) implies r = sup seq )

proof

assume A7: ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) ; :: thesis: r = sup seq

A8: now

let r1 be real number ; :: thesis: ( r1 in rng seq implies r1 <= r )
assume r1 in rng seq ; :: thesis: r1 <= r
then ex n being set st
( n in dom seq & seq . n = r1 ) by FUNCT_1:def 5;
hence r1 <= r by A7; :: thesis: verum

end;

now

let s be real number ; :: thesis: ( 0 < s implies ex r2 being real number st
( r2 in rng seq & r - s < r2 ) )
assume 0 < s ; :: thesis: ex r2 being real number st
( r2 in rng seq & r - s < r2 )
then consider k being Element of NAT such that
A9: r - s < seq . k by A7;
consider r2 being real number such that
A10: ( r2 in rng seq & r2 = seq . k ) by FUNCT_2:6;
take r2 = r2; :: thesis: ( r2 in rng seq & r - s < r2 )
thus ( r2 in rng seq & r - s < r2 ) by A9, A10; :: thesis: verum

end;

hence r = sup seq by A1, A8, SEQ_4:def 4; :: thesis: verum

end;

hence ( r = sup seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) ) by A2; :: thesis: verum