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
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }