theorem Th6: :: CARD_LAR:6

for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) )