theorem Th16: :: CARD_2:17

for x, y being object
for X, Y being set st x <> y holds
(card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])