let n be Nat; :: thesis: for seq being Real_Sequence st seq is bounded_below holds
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) )
reconsider Y2 = { (seq . k) where k is Nat : n + 1 <= k } as Subset of REAL by Th29;
reconsider Y1 = { (seq . k) where k is Nat : n <= k } as Subset of REAL by Th29;
reconsider Y3 = {(seq . n)} as Subset of REAL ;
A1: (inferior_realsequence seq) . (n + 1) = lower_bound Y2 by Def4;
assume A2: seq is bounded_below ; :: thesis: (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
then A3: ( Y2 <> {} & Y2 is bounded_below ) by Th32, SETLIM_1:1;
A4: Y3 is bounded_below

proof

consider t being Real such that
A5: for m being Nat holds t < seq . m by A2, SEQ_2:def 4;
t is LowerBound of Y3

proof

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in Y3 or t <= r )
assume r in Y3 ; :: thesis: t <= r
then r = seq . n by TARSKI:def 1;
hence t <= r by A5; :: thesis: verum

end;

hence Y3 is bounded_below ; :: thesis: verum

end;

(inferior_realsequence seq) . n = lower_bound Y1 by Def4;
then (inferior_realsequence seq) . n = lower_bound (Y2 \/ Y3) by SETLIM_1:2
.= min ((lower_bound Y2),(lower_bound Y3)) by A3, A4, SEQ_4:142
.= min (((inferior_realsequence seq) . (n + 1)),(seq . n)) by A1, SEQ_4:9 ;
hence (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) ; :: thesis: verum