theorem Th23: :: GLIBPRE0:19

for X, Y being set st card X = card Y holds
card (2Set X) = card (2Set Y)