let psi be Ordinal-Sequence; :: thesis: rng psi c= sup psi
let e be object ; :: 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 Th48;
hence e in sup psi by A1, Th19; :: thesis: verum