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 A2: s in rng rseq ; :: thesis: s <= K
consider n being set such that
A3: ( n in NAT & rseq . n = s ) by A2, FUNCT_2:17;
thus s <= K by A1, A3; :: thesis: verum

end;

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