theorem :: SYSREL:5

for X, Y being set holds [:X,Y:] ~ = [:Y,X:]