["P,R"] c= [:[:A,X:],[:B,Y:]:]

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ["P,R"] or q in [:[:A,X:],[:B,Y:]:] )
assume A1: q in ["P,R"] ; :: thesis: q in [:[:A,X:],[:B,Y:]:]
then [((q `1 ) `1 ),((q `2 ) `1 )] in P by Th10;
then consider x, y being set such that
A2: ( [((q `1 ) `1 ),((q `2 ) `1 )] = [x,y] & x in A & y in B ) by RELSET_1:6;
[((q `1 ) `2 ),((q `2 ) `2 )] in R by A1, Th10;
then consider s, t being set such that
A3: ( [((q `1 ) `2 ),((q `2 ) `2 )] = [s,t] & s in X & t in Y ) by RELSET_1:6;
consider a, b being set such that
A4: q = [a,b] by A1, Th10;
consider a1, b1 being set such that
A5: q `1 = [a1,b1] by A1, Th10;
consider a2, b2 being set such that
A6: q `2 = [a2,b2] by A1, Th10;
A7: ( a = [a1,b1] & b = [a2,b2] ) by A4, A5, A6, MCART_1:7;
then A8: a `1 = x by A2, A5, ZFMISC_1:33;
A9: a `2 = s by A3, A5, A7, ZFMISC_1:33;
A10: b `1 = y by A2, A6, A7, ZFMISC_1:33;
b `2 = t by A3, A6, A7, ZFMISC_1:33;
then ( a in [:A,X:] & b in [:B,Y:] ) by A2, A3, A7, A8, A9, A10, MCART_1:11;
hence q in [:[:A,X:],[:B,Y:]:] by A4, ZFMISC_1:def 2; :: thesis: verum

end;

hence ["P,R"] is Relation of [:A,X:],[:B,Y:] by RELSET_1:def 1; :: thesis: verum