theorem Th5: :: CARD_2:5

for X, Y, Z being set holds
( [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] )