let A be non empty set ; :: thesis: for R being Relation of [:A,A:] holds id A is_automorphism_of R
let R be Relation of [:A,A:]; :: thesis: id A is_automorphism_of R
let x be Element of A; :: according to TRANSGEO:def 3 :: thesis: for y, z, t being Element of A holds
( [[x,y],[z,t]] in R iff [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R )
let y, z, t be Element of A; :: thesis: ( [[x,y],[z,t]] in R iff [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R )
A1: (id A) . z = z by FUNCT_1:18;
A2: ( (id A) . x = x & (id A) . y = y ) by FUNCT_1:18;
hence ( [[x,y],[z,t]] in R implies [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R ) by A1, FUNCT_1:18; :: thesis: ( [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R implies [[x,y],[z,t]] in R )
assume [[((id A) . x),((id A) . y)],[((id A) . z),((id A) . t)]] in R ; :: thesis: [[x,y],[z,t]] in R
hence [[x,y],[z,t]] in R by A2, A1, FUNCT_1:18; :: thesis: verum