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: R [*] is_symmetric_in X

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 A2, FINSEQ_1:def 17;
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 A2, FINSEQ_1:def 17;
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 A10, XREAL_1:10;
j <= len p by A8, A11, FINSEQ_5:def 3;
then j in Seg (len p) by A10, FINSEQ_1:1;
then j in dom p by FINSEQ_1:def 3;
then A13: r . j = p . (((len p) - j) + 1) by A8, FINSEQ_5:58;
A14: j < len p by A8, A11, FINSEQ_5:def 3;
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 A15, FINSEQ_1:1;
then A16: j + 1 in dom p by FINSEQ_1:def 3;
(len p) - j is Nat by A14, NAT_1:21;
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 A15, A17, XREAL_1:19;
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 A1, A18, RELAT_2:def 3;
hence [(r . j),(r . (j + 1))] in R by A8, A16, A13, FINSEQ_5:58; :: thesis: verum

end;

A19: r . (len r) = r . (len p) by A8, FINSEQ_5:def 3
.= x by A5, A8, FINSEQ_5:62 ;
( len r >= 1 & r . 1 = y ) by A4, A6, A8, FINSEQ_5:62, FINSEQ_5:def 3;
hence [y,x] in R [*] by A3, A19, A9, FINSEQ_1:def 17; :: thesis: verum

end;

hence R [*] is_symmetric_in X by RELAT_2:def 3; :: thesis: verum