for n being Nat
for r being Real
for seq being Real_Sequence st seq is V96() holds
( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )