theorem Th7: :: CARD_2:8

for X1, X2, Y1, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds
( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] )