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

assume A3: r < sup seq ; :: thesis: contradiction
set r1 = (sup seq) - r;
(sup seq) - r > 0 by A3, XREAL_1:52;
then consider k being Element of NAT such that
A4: (sup seq) - ((sup seq) - r) < seq . k by A2, Th7;
thus contradiction by A1, A4; :: thesis: verum

end;

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

end;

assume A5: ( seq is bounded_above & 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 A5, Th7;
hence seq . n <= r by A5, XXREAL_0:2; :: thesis: verum

end;

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