let A be non empty set ; :: thesis: for f being Permutation of A

for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_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 ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds

f is_automorphism_of R

let R be Relation of [:A,A:]; :: thesis: ( ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f is_automorphism_of R )

assume that

A1: for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R and

A2: for x, y, z being Element of A holds [[x,x],[y,z]] in R and

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

[y,x] in R and

A4: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to RELAT_2:def 3,TRANSGEO:def 2 :: thesis: f is_automorphism_of R

A5: for x, y, z being Element of A holds [[y,z],[x,x]] in R

( [[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 )

A7: [[x,y],[(f . x),(f . y)]] in R by A4;

A8: [[z,t],[(f . z),(f . t)]] in R by A4;

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

then A9: [[(f . z),(f . t)],[z,t]] in R by A3, A8;

then A16: [[(f . x),(f . y)],[x,y]] in R by A3, A7;

for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_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 ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds

f is_automorphism_of R

let R be Relation of [:A,A:]; :: thesis: ( ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f is_automorphism_of R )

assume that

A1: for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a <> b holds

[[x,y],[z,t]] in R and

A2: for x, y, z being Element of A holds [[x,x],[y,z]] in R and

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

[y,x] in R and

A4: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to RELAT_2:def 3,TRANSGEO:def 2 :: thesis: f is_automorphism_of R

A5: for x, y, z being Element of A holds [[y,z],[x,x]] in R

proof

let x be Element of A; :: according to TRANSGEO:def 3 :: thesis: for y, z, t being Element of A holds
let x, y, z be Element of A; :: thesis: [[y,z],[x,x]] in R

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

[[x,x],[y,z]] in R by A2;

hence [[y,z],[x,x]] in R by A3, A6; :: thesis: verum

end;A6: ( [y,z] in [:A,A:] & [x,x] in [:A,A:] ) by ZFMISC_1:def 2;

[[x,x],[y,z]] in R by A2;

hence [[y,z],[x,x]] in R by A3, A6; :: thesis: verum

( [[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 )

A7: [[x,y],[(f . x),(f . y)]] in R by A4;

A8: [[z,t],[(f . z),(f . t)]] in R by A4;

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

then A9: [[(f . z),(f . t)],[z,t]] in R by A3, A8;

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

( [x,y] in [:A,A:] & [(f . x),(f . y)] in [:A,A:] )
by ZFMISC_1:def 2;assume A11:
[[(f . x),(f . y)],[(f . z),(f . t)]] in R
; :: thesis: [[x,y],[z,t]] in R

end;A12: now :: thesis: ( f . x <> f . y & f . z <> f . t implies [[x,y],[z,t]] in R )

assume that

A13: f . x <> f . y and

A14: f . z <> f . t ; :: thesis: [[x,y],[z,t]] in R

[[x,y],[(f . z),(f . t)]] in R by A1, A7, A11, A13;

hence [[x,y],[z,t]] in R by A1, A9, A14; :: thesis: verum

end;A13: f . x <> f . y and

A14: f . z <> f . t ; :: thesis: [[x,y],[z,t]] in R

[[x,y],[(f . z),(f . t)]] in R by A1, A7, A11, A13;

hence [[x,y],[z,t]] in R by A1, A9, A14; :: thesis: verum

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

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

then z = t by FUNCT_2:58;

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

end;then z = t by FUNCT_2:58;

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

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

hence
[[x,y],[z,t]] in R
by A15, A12; :: thesis: verumassume
f . x = f . y
; :: thesis: [[x,y],[z,t]] in R

then x = y by FUNCT_2:58;

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

end;then x = y by FUNCT_2:58;

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

then A16: [[(f . x),(f . y)],[x,y]] in R by A3, A7;

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 A10; :: thesis: verumassume A17:
[[x,y],[z,t]] in R
; :: thesis: [[(f . x),(f . y)],[(f . z),(f . t)]] in R

end;now :: thesis: ( x <> y & z <> t implies [[(f . x),(f . y)],[(f . z),(f . t)]] in R )

hence
[[(f . x),(f . y)],[(f . z),(f . t)]] in R
by A2, A5; :: thesis: verumassume that

A18: x <> y and

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

[[(f . x),(f . y)],[z,t]] in R by A1, A16, A17, A18;

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

end;A18: x <> y and

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

[[(f . x),(f . y)],[z,t]] in R by A1, A16, A17, A18;

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