let X, Y be finite set ; :: thesis: ( ( 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; :: thesis: verum

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; :: thesis: verum