for e being set
for psi being Ordinal-Sequence st e in rng psi holds
e is Ordinal by ORDINAL2:48;