theorem Th7: :: CARD_LAR:7

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