for A being limit_ordinal infinite Ordinal
for X being Subset of A st X is unbounded holds
not X is empty