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