let X be set ; :: thesis: ( not X is finite implies ( [:X,X:],X are_equipotent & card [:X,X:] = card X ) )
assume not X is finite ; :: thesis: ( [: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; :: thesis: verum