theorem :: TRANSGEO:21

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