for psi being Ordinal-Sequence holds rng psi c= sup psi by ORDINAL2:49;