theorem Th87: :: ZFMISC_1:88

for x, y being object
for X, Y being set st [x,y] in [:X,Y:] holds
[y,x] in [:Y,X:]