theorem :: GLIBPRE0:12

for x, y being object holds {[x,y]} ~ = {[y,x]}