for seq being Real_Sequence st seq is V95() holds
superior_realsequence seq = - (inferior_realsequence (- seq))