let n be Element of NAT ; :: thesis: for r being real number
for seq being Real_Sequence st seq is bounded_above holds
( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
let r be real number ; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) ) )
assume A1: seq is bounded_above ; :: thesis: ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29;
A2: ( not Y1 is empty & Y1 is bounded_above ) by A1, Th31, SETLIM_1:1;
thus ( r = (superior_realsequence seq) . n implies ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) ) :: thesis: ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) implies r = (superior_realsequence seq) . n )

proof

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

proof

let k be Element of NAT ; :: thesis: seq . (n + k) <= r
seq . (n + k) in Y1 by SETLIM_1:1;
hence seq . (n + k) <= r by A2, A3, SEQ_4:def 4; :: thesis: verum

end;

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

proof

let s be real number ; :: thesis: ( 0 < s implies ex k being Element of NAT st r - s < seq . (n + k) )
assume A5: 0 < s ; :: thesis: ex k being Element of NAT st r - s < seq . (n + k)
consider r1 being real number such that
A6: ( r1 in Y1 & r - s < r1 ) by A2, A3, A5, SEQ_4:def 4;
consider k1 being Element of NAT such that
A7: ( r1 = seq . k1 & n <= k1 ) by A6;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
k2 in NAT by ORDINAL1:def 13;
hence ex k being Element of NAT st r - s < seq . (n + k) by A6, A7, A8; :: thesis: verum

end;

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

end;

assume that
A9: for k being Element of NAT holds seq . (n + k) <= r and
A10: for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ; :: thesis: r = (superior_realsequence seq) . n
A11: for r1 being real number st r1 in Y1 holds
r1 <= r

proof

let r1 be real number ; :: thesis: ( r1 in Y1 implies r1 <= r )
assume A12: r1 in Y1 ; :: thesis: r1 <= r
consider k1 being Element of NAT such that
A13: ( r1 = seq . k1 & n <= k1 ) by A12;
consider k2 being Nat such that
A14: k1 = n + k2 by A13, NAT_1:10;
k2 in NAT by ORDINAL1:def 13;
hence r1 <= r by A9, A13, A14; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r1 being real number st
( r1 in Y1 & r - s < r1 )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r1 being real number st
( r1 in Y1 & r - s < r1 ) )
assume A15: 0 < s ; :: thesis: ex r1 being real number st
( r1 in Y1 & r - s < r1 )
consider k being Element of NAT such that
A16: r - s < seq . (n + k) by A10, A15;
n + k >= n by NAT_1:11;
then seq . (n + k) in Y1 ;
then consider r1 being real number such that
A17: ( r1 in Y1 & r1 = seq . (n + k) ) ;
thus ex r1 being real number st
( r1 in Y1 & r - s < r1 ) by A16, A17; :: thesis: verum

end;

then r = sup Y1 by A2, A11, SEQ_4:def 4;
hence r = (superior_realsequence seq) . n by Def5; :: thesis: verum