let seq be Real_Sequence; :: thesis: ( seq is bounded implies for n being Element of NAT
for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds
R is bounded )
assume A1: seq is bounded ; :: thesis: for n being Element of NAT
for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds
R is bounded
let n be Element of NAT ; :: thesis: for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds
R is bounded
let R be Subset of REAL ; :: thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies R is bounded )
assume R = { (seq . k) where k is Element of NAT : n <= k } ; :: thesis: R is bounded
then ( R is bounded_above & R is bounded_below ) by A1, Th31, Th32;
hence R is bounded by XXREAL_2:def 11; :: thesis: verum