let n be Nat; :: thesis: for r being Real
for seq being Real_Sequence st seq is bounded_above holds
( ( for m being Nat st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
let r be Real; :: thesis: for seq being Real_Sequence st seq is bounded_above holds
( ( for m being Nat st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
let seq be Real_Sequence; :: thesis: ( seq is bounded_above implies ( ( for m being Nat st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r ) )
assume A1: seq is bounded_above ; :: thesis: ( ( for m being Nat st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
thus ( ( for m being Nat st n <= m holds
seq . m <= r ) implies (superior_realsequence seq) . n <= r ) :: thesis: ( (superior_realsequence seq) . n <= r implies for m being Nat st n <= m holds
seq . m <= r )

proof

assume for m being Nat st n <= m holds
seq . m <= r ; :: thesis: (superior_realsequence seq) . n <= r
then for k being Nat holds seq . (n + k) <= r by NAT_1:11;
hence (superior_realsequence seq) . n <= r by A1, Th44; :: thesis: verum

end;

assume A2: (superior_realsequence seq) . n <= r ; :: thesis: for m being Nat st n <= m holds
seq . m <= r

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

let m be Nat; :: thesis: ( n <= m implies seq . m <= r )
assume n <= m ; :: thesis: seq . m <= r
then consider k being Nat such that
A3: m = n + k by NAT_1:10;
thus seq . m <= r by A1, A2, A3, Th44; :: thesis: verum

end;

hence for m being Nat st n <= m holds
seq . m <= r ; :: thesis: verum