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

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