let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_below )
assume A1: seq is bounded_below ; :: thesis: for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_below
let n be Nat; :: thesis: for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_below
set seq1 = seq ^\ n;
seq ^\ n is bounded_below by A1, SEQM_3:28;
then A2: rng (seq ^\ n) is bounded_below by Th6;
let R be Subset of REAL; :: thesis: ( R = { (seq . k) where k is Nat : n <= k } implies R is bounded_below )
assume R = { (seq . k) where k is Nat : n <= k } ; :: thesis: R is bounded_below
hence R is bounded_below by A2, Th30; :: thesis: verum