for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) = card X