theorem Th7: :: CHAIN_1:8

for X, Y being finite set holds
( ( card X is even iff card Y is even ) iff card (X \+\ Y) is even )