let X, Y be set ; :: thesis: [:X,Y:] ~ = [:Y,X:]
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in [:X,Y:] ~ or [x,b₁] in [:Y,X:] ) & ( not [x,b₁] in [:Y,X:] or [x,b₁] in [:X,Y:] ~ ) )
let y be set ; :: thesis: ( ( 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:] ) :: thesis: ( not [x,y] in [:Y,X:] or [x,y] in [:X,Y:] ~ )

proof

assume [x,y] in [:X,Y:] ~ ; :: thesis: [x,y] in [:Y,X:]
then [y,x] in [:X,Y:] by RELAT_1:def 7;
then ( y in X & x in Y ) by ZFMISC_1:106;
hence [x,y] in [:Y,X:] by ZFMISC_1:106; :: thesis: verum

end;

assume [x,y] in [:Y,X:] ; :: thesis: [x,y] in [:X,Y:] ~
then ( y in X & x in Y ) by ZFMISC_1:106;
then [y,x] in [:X,Y:] by ZFMISC_1:106;
hence [x,y] in [:X,Y:] ~ by RELAT_1:def 7; :: thesis: verum