theorem :: CARD_1:68

for X, Y being set st card X in card Y holds
Y \ X <> {}