let X, Y be set ; :: thesis: ( X c= Y implies Lim X c= Lim Y )
assume A1: X c= Y ; :: thesis: Lim X c= Lim Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim X or x in Lim Y )
assume x in Lim X ; :: thesis: x in Lim Y
then ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) by ORDINAL1:def 10;
hence x in Lim Y by A1, ORDINAL1:def 10; :: thesis: verum