for n being Nat
for seq being ExtREAL_sequence holds
( inf seq <= seq . n & seq . n <= sup seq )