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