let F be Subset of omega; :: thesis: card F c= order_type_of (RelIncl F)
card F = card (order_type_of (RelIncl F)) by Th7;
hence card F c= order_type_of (RelIncl F) by CARD_1:8; :: thesis: verum