for A being Ordinal
for X being set st X c= A holds
sup X is_cofinal_with order_type_of (RelIncl X)