let r be Real; :: thesis: for seq being Real_Sequence holds
( ( for n being Nat holds seq . n <= r ) iff ( seq is bounded_above & upper_bound seq <= r ) )
let seq be Real_Sequence; :: thesis: ( ( for n being Nat holds seq . n <= r ) iff ( seq is bounded_above & upper_bound seq <= r ) )
thus ( ( for n being Nat holds seq . n <= r ) implies ( seq is bounded_above & upper_bound seq <= r ) ) :: thesis: ( seq is bounded_above & upper_bound seq <= r implies for n being Nat holds seq . n <= r )

proof

assume A1: for n being Nat holds seq . n <= r ; :: thesis: ( seq is bounded_above & upper_bound seq <= r )

now :: thesis: for m being Nat holds seq . m < r + 1

let m be Nat; :: thesis: seq . m < r + 1
seq . m <= r by A1;
hence seq . m < r + 1 by Lm1; :: thesis: verum

end;

hence A2: seq is bounded_above by SEQ_2:def 3; :: thesis: upper_bound seq <= r

now :: thesis: not r < upper_bound seq

set r1 = (upper_bound seq) - r;
assume r < upper_bound seq ; :: thesis: contradiction
then (upper_bound seq) - r > 0 by XREAL_1:50;
then ex k being Nat st (upper_bound seq) - ((upper_bound seq) - r) < seq . k by A2, Th7;
hence contradiction by A1; :: thesis: verum

end;

hence upper_bound seq <= r ; :: thesis: verum

end;

assume that
A3: seq is bounded_above and
A4: upper_bound seq <= r ; :: thesis: for n being Nat holds seq . n <= r

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

let n be Nat; :: thesis: seq . n <= r
seq . n <= upper_bound seq by A3, Th7;
hence seq . n <= r by A4, XXREAL_0:2; :: thesis: verum

end;

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