:: deftheorem defines unbounded CARD_LAR:def 4 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff sup X = A );