let X, Y be finite set ; :: thesis: card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y))
A1: card (X \/ (Y \ X)) = (card X) + (card (Y \ X)) by Th53, XBOOLE_1:79;
( Y \ X = Y \ (X /\ Y) & X /\ Y c= Y ) by XBOOLE_1:17, XBOOLE_1:47;
then ( card (Y \ X) = (card Y) - (card (X /\ Y)) & X \/ (Y \ X) = X \/ Y ) by Th63, XBOOLE_1:39;
hence card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y)) by A1; :: thesis: verum