theorem :: RINFSUP1:11

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