for A being limit_ordinal infinite Ordinal
for X being Subset of A st not X is empty & ( for B1 being Ordinal st B1 in X holds
ex B2 being Ordinal st
( B2 in X & B1 in B2 ) ) holds
sup X is limit_ordinal infinite Ordinal