theorem :: TRANSGEO:19

for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R holds
f is_automorphism_of R