theorem :: WELLORD2:14

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