let X, Y be finite set ; :: thesis: card (X \/ Y) <= (card X) + (card Y)
( card X = card (card X) & card Y = card (card Y) ) ;
then (card X) +` (card Y) = card ((card X) + (card Y)) by Th37;
then ( card (Segm (card (X \/ Y))) = card (X \/ Y) & card (X \/ Y) c= card (Segm ((card X) + (card Y))) ) by Th33;
hence card (X \/ Y) <= (card X) + (card Y) by NAT_1:40; :: thesis: verum