theorem :: RINFSUP1:12

for seq being Real_Sequence holds
( seq is bounded_below iff - seq is bounded_above )