let X be set ; :: thesis: for x, y being object

for R being symmetric Relation of X st [x,y] in R holds

[y,x] in R

let x, y be object ; :: thesis: for R being symmetric Relation of X st [x,y] in R holds

[y,x] in R

let R be symmetric Relation of X; :: thesis: ( [x,y] in R implies [y,x] in R )

assume A1: [x,y] in R ; :: thesis: [y,x] in R

then ( x in field R & y in field R ) by RELAT_1:15;

hence [y,x] in R by A1, RELAT_2:def 3, RELAT_2:def 11; :: thesis: verum

for R being symmetric Relation of X st [x,y] in R holds

[y,x] in R

let x, y be object ; :: thesis: for R being symmetric Relation of X st [x,y] in R holds

[y,x] in R

let R be symmetric Relation of X; :: thesis: ( [x,y] in R implies [y,x] in R )

assume A1: [x,y] in R ; :: thesis: [y,x] in R

then ( x in field R & y in field R ) by RELAT_1:15;

hence [y,x] in R by A1, RELAT_2:def 3, RELAT_2:def 11; :: thesis: verum