:: deftheorem defines limit_ordinal ORDINAL1:def 6 :
for A being set holds
( A is limit_ordinal iff A = union A );