let X be set ; :: thesis: for R being Relation of X st R is_symmetric_in X holds
R [*] is_symmetric_in X

let R be Relation of X; :: thesis: ( R is_symmetric_in X implies R [*] is_symmetric_in X )
assume A1: R is_symmetric_in X ; :: thesis:
now :: thesis: for x, y being object st x in X & y in X & [x,y] in R [*] holds
[y,x] in R [*]
let x, y be object ; :: thesis: ( x in X & y in X & [x,y] in R [*] implies [y,x] in R [*] )
assume that
x in X and
y in X and
A2: [x,y] in R [*] ; :: thesis: [y,x] in R [*]
A3: ( x in field R & y in field R ) by ;
consider p being FinSequence such that
A4: len p >= 1 and
A5: p . 1 = x and
A6: p . (len p) = y and
A7: for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R by ;
consider r being FinSequence such that
A8: r = Rev p ;
A9: now :: thesis: for j being Nat st j >= 1 & j < len r holds
[(r . j),(r . (j + 1))] in R
let j be Nat; :: thesis: ( j >= 1 & j < len r implies [(r . j),(r . (j + 1))] in R )
assume that
A10: j >= 1 and
A11: j < len r ; :: thesis: [(r . j),(r . (j + 1))] in R
A12: (len p) - 0 > (len p) - j by ;
j <= len p by ;
then j in Seg (len p) by ;
then j in dom p by FINSEQ_1:def 3;
then A13: r . j = p . (((len p) - j) + 1) by ;
A14: j < len p by ;
then A15: len p >= j + 1 by NAT_1:13;
j + 1 >= 1 by NAT_1:11;
then j + 1 in Seg (len p) by ;
then A16: j + 1 in dom p by FINSEQ_1:def 3;
(len p) - j is Nat by ;
then (len p) - j in NAT by ORDINAL1:def 12;
then consider j1 being Element of NAT such that
A17: j1 = (len p) - j ;
j1 >= 1 by ;
then A18: [(p . ((len p) - j)),(p . (((len p) - j) + 1))] in R by A7, A17, A12;
then ( p . ((len p) - j) in X & p . (((len p) - j) + 1) in X ) by ZFMISC_1:87;
then [(p . (((len p) - j) + 1)),(p . (((len p) - (j + 1)) + 1))] in R by ;
hence [(r . j),(r . (j + 1))] in R by ; :: thesis: verum
end;
A19: r . (len r) = r . (len p) by
.= x by ;
( len r >= 1 & r . 1 = y ) by ;
hence [y,x] in R [*] by ; :: thesis: verum
end;
hence R [*] is_symmetric_in X by RELAT_2:def 3; :: thesis: verum