theorem Th11: :: KNASTER:11

for X, Y being non empty set
for f being Function of X,Y st f is bijective holds
X,Y are_equipotent