for X, Y being set st X,Y are_equipotent & X is finite holds
Y is finite