theorem Th4: :: CARD_2:4

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