let X, Y be finite set ; :: thesis: ( ( card X is even iff card Y is even ) iff card (X \+\ Y) is even )
( X \ Y misses X /\ Y & X = (X \ Y) \/ (X /\ Y) & Y \ X misses X /\ Y & Y = (Y \ X) \/ (X /\ Y) & X \ Y misses Y \ X & X \+\ Y = (X \ Y) \/ (Y \ X) ) by XBOOLE_0:def 6, XBOOLE_1:51, XBOOLE_1:82, XBOOLE_1:89;
then ( not ( ( card (X \ Y) is even implies card (X /\ Y) is even ) & ( card (X /\ Y) is even implies card (X \ Y) is even ) & not card X is even ) & ( card X is even implies ( card (X \ Y) is even iff card (X /\ Y) is even ) ) & not ( ( card (Y \ X) is even implies card (X /\ Y) is even ) & ( card (X /\ Y) is even implies card (Y \ X) is even ) & not card Y is even ) & ( card Y is even implies ( card (Y \ X) is even iff card (X /\ Y) is even ) ) & not ( ( card (X \ Y) is even implies card (Y \ X) is even ) & ( card (Y \ X) is even implies card (X \ Y) is even ) & not card (X \+\ Y) is even ) & ( card (X \+\ Y) is even implies ( card (X \ Y) is even iff card (Y \ X) is even ) ) ) by Th8;
hence ( ( card X is even iff card Y is even ) iff card (X \+\ Y) is even ) ; :: thesis: verum