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;
A1: card (LocNums F) = card (order_type_of (RelIncl (LocNums F))) by CARD_5:16;
F, LocNums F are_equipotent by Th27;
then card F = card (LocNums F) by CARD_1:21;
hence card F c= order_type_of (RelIncl (LocNums F)) by A1, CARD_1:24; :: thesis: verum