theorem :: ZFREFLE1:18

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