for A being limit_ordinal infinite Ordinal
for B1, B3 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1