theorem Th4: :: EULER_1:4

for A being finite set
for x being set st x in A holds
card (A \ {x}) = (card A) - (card {x}) by CARD_2:44, ZFMISC_1:31;