let x1, x2, y1, y2 be object ; :: thesis: for X1, X2, Y1, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 holds
( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
let 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 that
A1: X1,Y1 are_equipotent and
A2: X2,Y2 are_equipotent and
A3: x1 <> x2 and
A4: y1 <> y2 ; :: thesis: ( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
{x2},{y2} are_equipotent by CARD_1:28;
then A5: [:X2,{x2}:],[:Y2,{y2}:] are_equipotent by A2, Th7;
A6: now :: thesis: not [:Y1,{y1}:] meets [:Y2,{y2}:]
assume [:Y1,{y1}:] meets [:Y2,{y2}:] ; :: thesis: contradiction
then consider y being object such that
A7: y in [:Y1,{y1}:] and
A8: y in [:Y2,{y2}:] by XBOOLE_0:3;
y `2 in {y1} by A7, MCART_1:10;
then A9: y `2 = y1 by TARSKI:def 1;
y `2 in {y2} by A8, MCART_1:10;
hence contradiction by A4, A9, TARSKI:def 1; :: thesis: verum
end;
A10: now :: thesis: not [:X1,{x1}:] meets [:X2,{x2}:]
assume [:X1,{x1}:] meets [:X2,{x2}:] ; :: thesis: contradiction
then consider x being object such that
A11: x in [:X1,{x1}:] and
A12: x in [:X2,{x2}:] by XBOOLE_0:3;
x `2 in {x1} by A11, MCART_1:10;
then A13: x `2 = x1 by TARSKI:def 1;
x `2 in {x2} by A12, MCART_1:10;
hence contradiction by A3, A13, TARSKI:def 1; :: thesis: verum
end;
{x1},{y1} are_equipotent by CARD_1:28;
then [:X1,{x1}:],[:Y1,{y1}:] are_equipotent by A1, Th7;
hence [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent by A5, A10, A6, CARD_1:31; :: 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:5; :: thesis: verum