theorem :: RINFSUP1:11

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