for n being Nat
for seq being Real_Sequence st seq is V54() & seq is V95() holds
( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )