let X, Y be set ; for R being Relation st R c= [:X,Y:] holds
R ~ c= [:Y,X:]
let R be Relation; ( R c= [:X,Y:] implies R ~ c= [:Y,X:] )
assume A1:
R c= [:X,Y:]
; R ~ c= [:Y,X:]
let z, t be object ; RELAT_1:def 3 ( not [z,t] in R ~ or [z,t] in [:Y,X:] )
assume
[z,t] in R ~
; [z,t] in [:Y,X:]
then
[t,z] in R
by RELAT_1:def 7;
then
( t in X & z in Y )
by A1, ZFMISC_1:87;
hence
[z,t] in [:Y,X:]
by ZFMISC_1:87; verum