for A being limit_ordinal Ordinal
for X being set st X c= A & sup X = A holds
union X = A