let psi be Ordinal-Sequence; :: thesis: rng psi c= sup psi
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in rng psi or e in sup psi )
assume A1: e in rng psi ; :: thesis: e in sup psi
then e is Ordinal by Th66;
hence e in sup psi by A1, Th27; :: thesis: verum