:: deftheorem Def11 defines omega ORDINAL1:def 11 :
for b₁ being set holds
( b₁ = omega iff ( {} in b₁ & b₁ is limit_ordinal & b₁ is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b₁ c= A ) ) );