theorem Th1: :: HALLMAR1:1

for X, Y being finite set holds (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y)