let X, Y be finite set ; :: thesis: (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y)
card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y)) by CARD_2:45;
hence (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y) ; :: thesis: verum