theorem :: ORDINAL2:49

for psi being Ordinal-Sequence holds rng psi c= sup psi