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