let X be set ; 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 ; for R being symmetric Relation of X st [x,y] in R holds
[y,x] in R
let R be symmetric Relation of X; ( [x,y] in R implies [y,x] in R )
assume A1:
[x,y] in R
; [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; verum