let rseq be Real_Sequence; :: thesis: for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
sup (rng rseq) <= K
let K be real number ; :: thesis: ( ( for n being Element of NAT holds rseq . n <= K ) implies sup (rng rseq) <= K )
assume A1: for n being Element of NAT holds rseq . n <= K ; :: thesis: sup (rng rseq) <= K

now

let s be real number ; :: thesis: ( s in rng rseq implies s <= K )
assume s in rng rseq ; :: thesis: s <= K
then ex n being set st
( n in NAT & rseq . n = s ) by FUNCT_2:17;
hence s <= K by A1; :: thesis: verum

end;

hence sup (rng rseq) <= K by SEQ_4:62; :: thesis: verum