let x, y be object ; :: thesis: for X, Y being set st x <> y holds
(card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
let 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 ) by CARD_1:def 2;
then card H<sub>4</sub>(X,Y,x,y) = card H<sub>4</sub>( card X, card Y,x,y) by A1, Th11;
hence (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:]) by A1, Lm1; :: thesis: verum