let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being IL-Subset of S holds card F c= order_type_of (RelIncl (LocNums F))
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being IL-Subset of S holds card F c= order_type_of (RelIncl (LocNums F))
let F be IL-Subset of S; :: thesis: card F c= order_type_of (RelIncl (LocNums F))
set X = LocNums F;
F, LocNums F are_equipotent by Th27;
then ( card (LocNums F) = card (order_type_of (RelIncl (LocNums F))) & card F = card (LocNums F) ) by CARD_1:21, CARD_5:16;
hence card F c= order_type_of (RelIncl (LocNums F)) by CARD_1:24; :: thesis: verum