:: deftheorem defines limpoints CARD_LAR:def 9 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X = { B1 where B1 is Element of A : ( B1 is infinite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } ;