theorem :: RINFSUP1:12

for seq being Real_Sequence holds
( seq is V96() iff - seq is V95() )