let n be Element of 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) )
assume A1: seq is bounded_below ; :: thesis: (inferior_realsequence seq) . n = min ((inferior_realsequence seq) . (n + 1)),(seq . n)
reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29;
A2: (inferior_realsequence seq) . n = inf Y1 by Def4;
reconsider Y2 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29;
A3: (inferior_realsequence seq) . (n + 1) = inf Y2 by Def4;
reconsider Y3 = {(seq . n)} as Subset of REAL ;
A4: ( Y1 <> {} & Y2 <> {} & Y3 <> {} ) by SETLIM_1:1;
A5: ( Y1 is bounded_below & Y2 is bounded_below ) by A1, Th32;
A6: Y3 is bounded_below

proof

consider t being real number such that
A7: for m being Element of NAT holds t < seq . m by A1, SEQ_2:def 4;

now

take t = t; :: thesis: for r being real number st r in Y3 holds
t <= r
let r be real number ; :: thesis: ( r in Y3 implies t <= r )
assume r in Y3 ; :: thesis: t <= r
then r = seq . n by TARSKI:def 1;
hence t <= r by A7; :: thesis: verum

end;

hence Y3 is bounded_below by SEQ_4:def 2; :: thesis: verum

end;

(inferior_realsequence seq) . n = inf (Y2 \/ Y3) by A2, SETLIM_1:2
.= min (inf Y2),(inf Y3) by A4, A5, A6, SPRECT_1:52
.= min ((inferior_realsequence seq) . (n + 1)),(seq . n) by A3, SEQ_4:22 ;
hence (inferior_realsequence seq) . n = min ((inferior_realsequence seq) . (n + 1)),(seq . n) ; :: thesis: verum