let X, Y be set ; :: thesis: ( X c= Y implies On X c= On Y )
assume A1: X c= Y ; :: thesis: On X c= On Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On X or x in On Y )
assume x in On X ; :: thesis: x in On Y
then ( x in X & x is Ordinal ) by ORDINAL1:def 9;
hence x in On Y by A1, ORDINAL1:def 9; :: thesis: verum