theorem :: ORDINAL2:26

for L being Sequence holds
( sup L = sup (rng L) & inf L = inf (rng L) ) ;