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 Th34
.= card ((card X) + (card Y)) by Th37 ;
hence card (X \/ Y) = (card X) + (card Y) ; :: thesis: verum