let X, Y be finite set ; ( ( card X is even iff card Y is even ) iff card (X \+\ Y) is even )
A1:
X \ Y misses X /\ Y
by XBOOLE_1:89;
A2:
X = (X \ Y) \/ (X /\ Y)
by XBOOLE_1:51;
A3:
Y \ X misses X /\ Y
by XBOOLE_1:89;
A4:
Y = (Y \ X) \/ (X /\ Y)
by XBOOLE_1:51;
A5:
X \ Y misses Y \ X
by XBOOLE_1:82;
A6:
X \+\ Y = (X \ Y) \/ (Y \ X)
by XBOOLE_0:def 6;
A7:
( ( card (X \ Y) is even iff card (X /\ Y) is even ) iff card X is even )
by A1, A2, Th6;
( ( card (Y \ X) is even iff card (X /\ Y) is even ) iff card Y is even )
by A3, A4, Th6;
hence
( ( card X is even iff card Y is even ) iff card (X \+\ Y) is even )
by A5, A6, A7, Th6; verum