let X be set ; ( not X is finite implies ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) )
assume
not X is finite
; ( [:X,X:],X are_equipotent & card [:X,X:] = card X )
then
(card X) *` (card X) = card X
by Th15;
then
card [:(card X),(card X):] = card X
by CARD_2:def 2;
then
card [:X,X:] = card X
by CARD_2:7;
hence
( [:X,X:],X are_equipotent & card [:X,X:] = card X )
by CARD_1:5; verum