:: deftheorem Def9 defines On ORDINAL1:def 9 :
for X, b₂ being set holds
( b₂ = On X iff for x being object holds
( x in b₂ iff ( x in X & x is Ordinal ) ) );