let x, y, X, Y be set ; :: thesis: ( x <> y implies (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:]) )
assume A1: x <> y ; :: thesis: (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
( X, card X are_equipotent & Y, card Y are_equipotent & 0 <> 1 ) by CARD_1:def 5;
then card H₄(X,Y,x,y) = card H₄( card X, card Y,x,y) by A1, Th23;
hence (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:]) by A1, Lm1; :: thesis: verum