let X, Y be set ; :: thesis: for R being Relation st R c= [:X,Y:] holds
R ~ c= [:Y,X:]
let R be Relation; :: thesis: ( R c= [:X,Y:] implies R ~ c= [:Y,X:] )
assume A1: R c= [:X,Y:] ; :: thesis: R ~ c= [:Y,X:]
let z be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [z,b₁] in R ~ or [z,b₁] in [:Y,X:] )
let t be set ; :: thesis: ( not [z,t] in R ~ or [z,t] in [:Y,X:] )
assume [z,t] in R ~ ; :: thesis: [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:106;
hence [z,t] in [:Y,X:] by ZFMISC_1:106; :: thesis: verum