let X, Y be set ; :: thesis: [:X,Y:] ~ = [:Y,X:]
let x, y be object ; :: according to RELAT_1:def 2 :: 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:87;
hence [x,y] in [:Y,X:] by ZFMISC_1:87; :: 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:87;
then [y,x] in [:X,Y:] by ZFMISC_1:87;
hence [x,y] in [:X,Y:] ~ by RELAT_1:def 7; :: thesis: verum