let seq, seq1 be Real_Sequence; :: thesis: ( seq is bounded_below & seq1 is subsequence of seq implies seq1 is bounded_below )
assume that
A1: seq is bounded_below and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is bounded_below
consider r1 being Real such that
A3: for n being Nat holds r1 < seq . n 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 4 :: thesis: for b₁ being set holds not seq1 . b₁ <= r
let n be Nat; :: thesis: not seq1 . n <= r
n in NAT by ORDINAL1:def 12;
then seq1 . n = seq . (Nseq . n) by A4, FUNCT_2:15;
hence r < seq1 . n by A3; :: thesis: verum