:: deftheorem defines Lim ORDINAL1:def 10 :
for X, b₂ being set holds
( b₂ = Lim X iff for x being object holds
( x in b₂ iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) );