theorem :: CARD_5:39

for F being Subset of omega holds card F c= order_type_of (RelIncl F)