theorem Th43: :: CARD_2:44

for X, Y being finite set st Y c= X holds
card (X \ Y) = (card X) - (card Y)