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
proof
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;
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 )
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 )
assume A11: [[(f . x),(f . y)],[(f . z),(f . t)]] in R ; :: thesis: [[x,y],[z,t]] in R
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;
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;
now :: thesis: ( f . x = f . y implies [[x,y],[z,t]] in R )
assume 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;
hence [[x,y],[z,t]] in R by A15, A12; :: thesis: verum
end;
( [x,y] in [:A,A:] & [(f . x),(f . y)] in [:A,A:] ) by ZFMISC_1:def 2;
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 )
assume A17: [[x,y],[z,t]] in R ; :: thesis: [[(f . x),(f . y)],[(f . z),(f . t)]] in R
now :: thesis: ( x <> y & z <> t implies [[(f . x),(f . y)],[(f . z),(f . t)]] in R )
assume 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;
hence [[(f . x),(f . y)],[(f . z),(f . t)]] in R by A2, A5; :: thesis: verum
end;
hence ( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) by A10; :: thesis: verum