for A, B being limit_ordinal infinite Ordinal
for X being Subset of A st not sup (X /\ B) = B holds
ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )