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