let n be Nat; :: thesis: for r being Real
for seq being Real_Sequence st seq is bounded_above holds
( r = (superior_realsequence seq) . n iff ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) ) )
let r be Real; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
( r = (superior_realsequence seq) . n iff ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being 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 Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) ) ) )
reconsider Y1 = { (seq . k) where k is Nat : n <= k } as Subset of REAL by Th29;
assume seq is bounded_above ; :: thesis: ( r = (superior_realsequence seq) . n iff ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) ) )
then A1: ( not Y1 is empty & Y1 is bounded_above ) by Th31, SETLIM_1:1;
thus ( r = (superior_realsequence seq) . n implies ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) ) ) :: thesis: ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) implies r = (superior_realsequence seq) . n )

proof

assume r = (superior_realsequence seq) . n ; :: thesis: ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) )
then A2: r = upper_bound Y1 by Def5;
A3: for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k)

proof

let s be Real; :: thesis: ( 0 < s implies ex k being Nat st r - s < seq . (n + k) )
assume 0 < s ; :: thesis: ex k being Nat st r - s < seq . (n + k)
then consider r1 being Real such that
A4: r1 in Y1 and
A5: r - s < r1 by A1, A2, SEQ_4:def 1;
consider k1 being Nat such that
A6: r1 = seq . k1 and
A7: n <= k1 by A4;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
thus ex k being Nat st r - s < seq . (n + k) by A5, A6, A8; :: thesis: verum

end;

for k being Nat holds seq . (n + k) <= r

proof

let k be Nat; :: thesis: seq . (n + k) <= r
seq . (n + k) in Y1 by SETLIM_1:1;
hence seq . (n + k) <= r by A1, A2, SEQ_4:def 1; :: thesis: verum

end;

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

end;

assume that
A9: for k being Nat holds seq . (n + k) <= r and
A10: for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ; :: thesis: r = (superior_realsequence seq) . n
A11: for s being Real st 0 < s holds
ex r1 being Real st
( r1 in Y1 & r - s < r1 )

proof

let s be Real; :: thesis: ( 0 < s implies ex r1 being Real st
( r1 in Y1 & r - s < r1 ) )
assume 0 < s ; :: thesis: ex r1 being Real st
( r1 in Y1 & r - s < r1 )
then consider k being Nat such that
A12: r - s < seq . (n + k) by A10;
n + k >= n by NAT_1:11;
then seq . (n + k) in Y1 ;
hence ex r1 being Real st
( r1 in Y1 & r - s < r1 ) by A12; :: thesis: verum

end;

for r1 being Real st r1 in Y1 holds
r1 <= r

proof

let r1 be Real; :: thesis: ( r1 in Y1 implies r1 <= r )
assume r1 in Y1 ; :: thesis: r1 <= r
then consider k1 being Nat such that
A13: r1 = seq . k1 and
A14: n <= k1 ;
consider k2 being Nat such that
A15: k1 = n + k2 by A14, NAT_1:10;
thus r1 <= r by A9, A13, A15; :: thesis: verum

end;

then r = upper_bound Y1 by A1, A11, SEQ_4:def 1;
hence r = (superior_realsequence seq) . n by Def5; :: thesis: verum