theorem Th42: :: CARD_2:43

for X, Y being finite set holds card (X \/ Y) <= (card X) + (card Y)