theorem Th10: :: RINFSUP1:10

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