theorem :: GRFUNC_1:20

for f being Function st f is one-to-one holds
for x, y being object holds
( [y,x] in f " iff [x,y] in f )