:: deftheorem defines stationary CARD_LAR:def 7 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is stationary iff for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty );