let X, Y be finite set ; :: thesis: ( X misses Y implies ( ( card X is even iff card Y is even ) iff card (X \/ Y) is even ) )
assume X misses Y ; :: thesis: ( ( card X is even iff card Y is even ) iff card (X \/ Y) is even )
then card (X \/ Y) = (card X) + (card Y) by CARD_2:40;
hence ( ( card X is even iff card Y is even ) iff card (X \/ Y) is even ) ; :: thesis: verum