for n being Nat
for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n