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