:: deftheorem defines closed CARD_LAR:def 5 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is closed iff for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X );