for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds
[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds
f is_automorphism_of R