theorem :: TRANSGEO:16

for A being non empty set
for R being Relation of [:A,A:] holds id A is_automorphism_of R ;