for A being limit_ordinal infinite Ordinal
for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
( LBound (B1,X) in X & B1 in LBound (B1,X) )