let A be non empty set ; :: thesis: 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

let f be Permutation of A; :: thesis: 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

let R be Relation of [:A,A:]; :: thesis: ( R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R implies f is_automorphism_of R )

assume that

A1: for x, y being object st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds

[y,x] in R and

A2: for x, y, z being object st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds

[x,z] in R and

A3: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to RELAT_2:def 3,RELAT_2:def 8,TRANSGEO:def 2 :: thesis: f 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 [[(f . x),(f . y)],[(f . z),(f . t)]] in R )

let y, z, t be Element of A; :: thesis: ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R )

A4: [z,t] in [:A,A:] by ZFMISC_1:def 2;

A5: [(f . z),(f . t)] in [:A,A:] by ZFMISC_1:def 2;

A6: [(f . x),(f . y)] in [:A,A:] by ZFMISC_1:def 2;

A7: [x,y] in [:A,A:] by ZFMISC_1:def 2;

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

let f be Permutation of A; :: thesis: 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

let R be Relation of [:A,A:]; :: thesis: ( R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R implies f is_automorphism_of R )

assume that

A1: for x, y being object st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds

[y,x] in R and

A2: for x, y, z being object st x in [:A,A:] & y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds

[x,z] in R and

A3: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to RELAT_2:def 3,RELAT_2:def 8,TRANSGEO:def 2 :: thesis: f 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 [[(f . x),(f . y)],[(f . z),(f . t)]] in R )

let y, z, t be Element of A; :: thesis: ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R )

A4: [z,t] in [:A,A:] by ZFMISC_1:def 2;

A5: [(f . z),(f . t)] in [:A,A:] by ZFMISC_1:def 2;

A6: [(f . x),(f . y)] in [:A,A:] by ZFMISC_1:def 2;

A7: [x,y] in [:A,A:] by ZFMISC_1:def 2;

A8: now :: thesis: ( [[(f . x),(f . y)],[(f . z),(f . t)]] in R implies [[x,y],[z,t]] in R )

[[z,t],[(f . z),(f . t)]] in R
by A3;

then A9: [[(f . z),(f . t)],[z,t]] in R by A1, A4, A5;

assume A10: [[(f . x),(f . y)],[(f . z),(f . t)]] in R ; :: thesis: [[x,y],[z,t]] in R

[[x,y],[(f . x),(f . y)]] in R by A3;

then [[x,y],[(f . z),(f . t)]] in R by A2, A7, A6, A5, A10;

hence [[x,y],[z,t]] in R by A2, A7, A4, A5, A9; :: thesis: verum

end;then A9: [[(f . z),(f . t)],[z,t]] in R by A1, A4, A5;

assume A10: [[(f . x),(f . y)],[(f . z),(f . t)]] in R ; :: thesis: [[x,y],[z,t]] in R

[[x,y],[(f . x),(f . y)]] in R by A3;

then [[x,y],[(f . z),(f . t)]] in R by A2, A7, A6, A5, A10;

hence [[x,y],[z,t]] in R by A2, A7, A4, A5, A9; :: thesis: verum

now :: thesis: ( [[x,y],[z,t]] in R implies [[(f . x),(f . y)],[(f . z),(f . t)]] in R )

hence
( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R )
by A8; :: thesis: verum
[[x,y],[(f . x),(f . y)]] in R
by A3;

then A11: [[(f . x),(f . y)],[x,y]] in R by A1, A7, A6;

A12: [[z,t],[(f . z),(f . t)]] in R by A3;

assume [[x,y],[z,t]] in R ; :: thesis: [[(f . x),(f . y)],[(f . z),(f . t)]] in R

then [[(f . x),(f . y)],[z,t]] in R by A2, A7, A4, A6, A11;

hence [[(f . x),(f . y)],[(f . z),(f . t)]] in R by A2, A4, A6, A5, A12; :: thesis: verum

end;then A11: [[(f . x),(f . y)],[x,y]] in R by A1, A7, A6;

A12: [[z,t],[(f . z),(f . t)]] in R by A3;

assume [[x,y],[z,t]] in R ; :: thesis: [[(f . x),(f . y)],[(f . z),(f . t)]] in R

then [[(f . x),(f . y)],[z,t]] in R by A2, A7, A4, A6, A11;

hence [[(f . x),(f . y)],[(f . z),(f . t)]] in R by A2, A4, A6, A5, A12; :: thesis: verum