let rseq be Real_Sequence; :: thesis: ( rseq is bounded implies for n being Nat holds rseq . n <= upper_bound (rng rseq) )
assume rseq is bounded ; :: thesis: for n being Nat holds rseq . n <= upper_bound (rng rseq)
then rng rseq is real-bounded by MEASURE6:39;
then A1: rng rseq is bounded_above ;
let n be Nat; :: thesis: rseq . n <= upper_bound (rng rseq)
A2: n in NAT by ORDINAL1:def 12;
NAT = dom rseq by FUNCT_2:def 1;
then rseq . n in rng rseq by FUNCT_1:3, A2;
hence rseq . n <= upper_bound (rng rseq) by A1, SEQ_4:def 1; :: thesis: verum