:: deftheorem defines is_closed_in CARD_LAR:def 2 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_closed_in A iff ( X c= A & ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) ) );