let X, Y be finite set ; :: thesis: card (X \/ Y) <= (card X) + (card Y)
A1: card (card (X \/ Y)) = card (X \/ Y) ;
( card X = card (card X) & card Y = card (card Y) ) ;
then (card X) +` (card Y) = card ((card X) + (card Y)) by Th51;
then card (X \/ Y) c= card ((card X) + (card Y)) by Th47;
hence card (X \/ Y) <= (card X) + (card Y) by A1, NAT_1:41; :: thesis: verum