theorem :: ROUGHIF2:2

for x1, x2 being finite set holds card (x1 \+\ x2) = (card (x1 \ x2)) + (card (x2 \ x1)) by CARD_2:40, XBOOLE_1:82;