:: deftheorem defines inf ORDINAL2:def 6 :
for L being Sequence holds inf L = inf (rng L);