now :: thesis: for x, y being object st [x,y] in R ~ holds

[x,y] in [:Y,X:]

hence
R ~ is Relation of Y,X
by RELAT_1:def 3; :: thesis: verum[x,y] in [:Y,X:]

let x, y be object ; :: thesis: ( [x,y] in R ~ implies [x,y] in [:Y,X:] )

assume [x,y] in R ~ ; :: thesis: [x,y] in [:Y,X:]

then [y,x] in R by RELAT_1:def 7;

hence [x,y] in [:Y,X:] by ZFMISC_1:88; :: thesis: verum

end;assume [x,y] in R ~ ; :: thesis: [x,y] in [:Y,X:]

then [y,x] in R by RELAT_1:def 7;

hence [x,y] in [:Y,X:] by ZFMISC_1:88; :: thesis: verum