theorem :: GLIBPRE0:13

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