:: deftheorem defines is_unbounded_in CARD_LAR:def 1 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_unbounded_in A iff ( X c= A & sup X = A ) );