A1: now

let x, y be set ; :: 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:107; :: thesis: verum

end;

reconsider P = [:Y,X:] as Relation ;
R ~ c= P by A1, RELAT_1:def 3;
hence R ~ is Relation of Y,X by Def1; :: thesis: verum