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:] & f is_FormalIz_of R holds
f " is_FormalIz_of R
let f be Permutation of A; :: thesis: for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds
f " is_FormalIz_of R
let R be Relation of [:A,A:]; :: thesis: ( R is_symmetric_in [:A,A:] & f is_FormalIz_of R implies f " is_FormalIz_of R )
assume A1: for x, y being object st x in [:A,A:] & y in [:A,A:] & [x,y] in R holds
[y,x] in R ; :: according to RELAT_2:def 3 :: thesis: ( not f is_FormalIz_of R or f " is_FormalIz_of R )
assume A2: for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R ; :: according to TRANSGEO:def 2 :: thesis: f " is_FormalIz_of R
let x be Element of A; :: according to TRANSGEO:def 2 :: thesis: for y being Element of A holds [[x,y],[((f ") . x),((f ") . y)]] in R
let y be Element of A; :: thesis: [[x,y],[((f ") . x),((f ") . y)]] in R
A3: [[((f ") . x),((f ") . y)],[(f . ((f ") . x)),(f . ((f ") . y))]] in R by A2;
A4: ( [((f ") . x),((f ") . y)] in [:A,A:] & [(f . ((f ") . x)),(f . ((f ") . y))] in [:A,A:] ) by ZFMISC_1:def 2;
( f . ((f ") . x) = x & f . ((f ") . y) = y ) by Th2;
hence [[x,y],[((f ") . x),((f ") . y)]] in R by A1, A3, A4; :: thesis: verum