let X, Y be finite set ; :: thesis: ( X misses Y implies card (X \/ Y) = (card X) + (card Y) )
assume X misses Y ; :: thesis: card (X \/ Y) = (card X) + (card Y)
then card (card (X \/ Y)) = (card (card X)) +` (card (card Y)) by Th48
.= card ((card X) + (card Y)) by Th51 ;
hence card (X \/ Y) = (card X) + (card Y) by CARD_1:71; :: thesis: verum