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