for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded & limpoints X is bounded holds
ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )