let X, M be set ; :: thesis: ( X,M are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )
A1: ( X,M are_equipotent implies ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) )

proof

assume ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; :: according to TARSKI:def 6 :: thesis: ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) )
hence ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; :: thesis: verum

end;

( ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) implies X,M are_equipotent )

proof

assume ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; :: thesis: X,M are_equipotent
hence ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ; :: according to TARSKI:def 6 :: thesis: verum

end;

hence ( X,M are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in M & [x,y] in Z ) ) & ( for y being set st y in M holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, z1, y, z2 being set st [x,z1] in Z & [y,z2] in Z holds
( x = y iff z1 = z2 ) ) ) ) by A1; :: thesis: verum