theorem Th1: :: CARD_LAR:1
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is_club_in A iff ( X is closed & X is unbounded ) )