for n being Nat
for seq being ExtREAL_sequence holds
( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )