let n be Nat; :: thesis: for r being Real
for seq being Real_Sequence st seq is bounded_below holds
( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
let r be Real; :: thesis: for seq being Real_Sequence st seq is bounded_below holds
( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies ( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n ) )
assume A1: seq is bounded_below ; :: thesis: ( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
thus ( ( for m being Nat st n <= m holds
r <= seq . m ) implies r <= (inferior_realsequence seq) . n ) :: thesis: ( r <= (inferior_realsequence seq) . n implies for m being Nat st n <= m holds
r <= seq . m )

proof

assume for m being Nat st n <= m holds
r <= seq . m ; :: thesis: r <= (inferior_realsequence seq) . n
then for k being Nat holds r <= seq . (n + k) by NAT_1:11;
hence r <= (inferior_realsequence seq) . n by A1, Th42; :: thesis: verum

end;

assume A2: r <= (inferior_realsequence seq) . n ; :: thesis: for m being Nat st n <= m holds
r <= seq . m

now :: thesis: for m being Nat st n <= m holds
r <= seq . m

let m be Nat; :: thesis: ( n <= m implies r <= seq . m )
assume n <= m ; :: thesis: r <= seq . m
then consider k being Nat such that
A3: m = n + k by NAT_1:10;
thus r <= seq . m by A1, A2, A3, Th42; :: thesis: verum

end;

hence for m being Nat st n <= m holds
r <= seq . m ; :: thesis: verum