for seq being ExtREAL_sequence holds inf seq <= sup seq