theorem Th9: :: RINFSUP1:9

for r being Real
for seq being Real_Sequence holds
( ( for n being Nat holds seq . n <= r ) iff ( seq is bounded_above & upper_bound seq <= r ) )