for seq being Real_Sequence st seq is V54() & seq is V95() holds
lower_bound (superior_realsequence seq) = upper_bound seq