let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies (inferior_realsequence seq) . 0 = lower_bound seq )
reconsider Y1 = { (seq . k) where k is Nat : 0 <= k } as Subset of REAL by Th29;
(inferior_realsequence seq) . 0 = lower_bound Y1 by Def4
.= lower_bound seq by SETLIM_1:5 ;
hence ( seq is bounded_below implies (inferior_realsequence seq) . 0 = lower_bound seq ) ; :: thesis: verum