theorem LemSym: :: PREFER_1:20

for R being Relation holds
( R is symmetric iff for x, y being object st [x,y] in R holds
[y,x] in R )