for X, W being set st W is subset-closed & X in W holds
( not X,W are_equipotent & card X in card W )