:: deftheorem defines are_equipotent TARSKI:def 6 :
for X, Y being set holds
( X,Y are_equipotent iff ex Z being set st
( ( for x being object st x in X holds
ex y being object st
( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds
ex x being object st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) ) );