let seq, seq1 be Real_Sequence; :: thesis: ( seq is bounded_above & seq1 is subsequence of seq implies seq1 is bounded_above )
assume that
A1: seq is bounded_above and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is bounded_above
consider r1 being Real such that
A3: for n being Nat holds seq . n < r1 by A1;
consider Nseq being increasing sequence of NAT such that
A4: seq1 = seq * Nseq by A2, VALUED_0:def 17;
take r = r1; :: according to SEQ_2:def 3 :: thesis: for b₁ being set holds not r <= seq1 . b₁
let n be Nat; :: thesis: not r <= seq1 . n
n in NAT by ORDINAL1:def 12;
then seq1 . n = seq . (Nseq . n) by A4, FUNCT_2:15;
hence seq1 . n < r by A3; :: thesis: verum