let X1, Y1, X2, Y2, x1, x2, y1, y2 be set ; :: thesis: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 implies ( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) ) )
assume A1: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 ) ; :: thesis: ( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
( {x1},{y1} are_equipotent & {x2},{y2} are_equipotent ) by CARD_1:48;
then A2: ( [:X1,{x1}:],[:Y1,{y1}:] are_equipotent & [:X2,{x2}:],[:Y2,{y2}:] are_equipotent ) by A1, Th15;

A3: now

assume [:X1,{x1}:] meets [:X2,{x2}:] ; :: thesis: contradiction
then consider x being set such that
A4: ( x in [:X1,{x1}:] & x in [:X2,{x2}:] ) by XBOOLE_0:3;
( x `2 in {x1} & x `2 in {x2} ) by A4, MCART_1:10;
then ( x `2 = x1 & x `2 = x2 ) by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

now

assume [:Y1,{y1}:] meets [:Y2,{y2}:] ; :: thesis: contradiction
then consider y being set such that
A5: ( y in [:Y1,{y1}:] & y in [:Y2,{y2}:] ) by XBOOLE_0:3;
( y `2 in {y1} & y `2 in {y2} ) by A5, MCART_1:10;
then ( y `2 = y1 & y `2 = y2 ) by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

hence [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent by A2, A3, CARD_1:58; :: thesis: card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:])
hence card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) by CARD_1:21; :: thesis: verum