let r be real number ; :: thesis: for seq being Real_Sequence holds
( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is bounded_above & sup seq <= r ) )
let seq be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is bounded_above & sup seq <= r ) )
thus ( ( for n being Element of NAT holds seq . n <= r ) implies ( seq is bounded_above & sup seq <= r ) ) :: thesis: ( seq is bounded_above & sup seq <= r implies for n being Element of NAT holds seq . n <= r )

proof

assume A1: for n being Element of NAT holds seq . n <= r ; :: thesis: ( seq is bounded_above & sup seq <= r )

now

let m be Element of 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: sup seq <= r

now

set r1 = (sup seq) - r;
assume r < sup seq ; :: thesis: contradiction
then (sup seq) - r > 0 by XREAL_1:52;
then ex k being Element of NAT st (sup seq) - ((sup seq) - r) < seq . k by A2, Th7;
hence contradiction by A1; :: thesis: verum

end;

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

end;

assume that
A3: seq is bounded_above and
A4: sup seq <= r ; :: thesis: for n being Element of NAT holds seq . n <= r

now

let n be Element of NAT ; :: thesis: seq . n <= r
seq . n <= sup seq by A3, Th7;
hence seq . n <= r by A4, XXREAL_0:2; :: thesis: verum

end;

hence for n being Element of NAT holds seq . n <= r ; :: thesis: verum