theorem Th13: :: TRANSGEO:13

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:] & f is_FormalIz_of R holds
f " is_FormalIz_of R