let X, Y be set ; [:X,Y:] ~ = [:Y,X:]
let x, y be object ; RELAT_1:def 2 ( ( not [x,y] in [:X,Y:] ~ or [x,y] in [:Y,X:] ) & ( not [x,y] in [:Y,X:] or [x,y] in [:X,Y:] ~ ) )
thus
( [x,y] in [:X,Y:] ~ implies [x,y] in [:Y,X:] )
( not [x,y] in [:Y,X:] or [x,y] in [:X,Y:] ~ )
assume
[x,y] in [:Y,X:]
; [x,y] in [:X,Y:] ~
then
( y in X & x in Y )
by ZFMISC_1:87;
then
[y,x] in [:X,Y:]
by ZFMISC_1:87;
hence
[x,y] in [:X,Y:] ~
by RELAT_1:def 7; verum