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

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 [*]

hence
R [*] is_symmetric_in X
by RELAT_2:def 3; :: thesis: verum[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 16;

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 16;

consider r being FinSequence such that

A8: r = Rev p ;

.= 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 16; :: thesis: verum

end;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 16;

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 16;

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

A19: r . (len r) =
r . (len p)
by A8, FINSEQ_5:def 3
[(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;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

.= 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 16; :: thesis: verum