["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 consider a, b being set such that
A2: q = [a,b] by Th10;
[((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] and
A4: s in X and
A5: t in Y by RELSET_1:6;
consider a2, b2 being set such that
A6: q `2 = [a2,b2] by A1, Th10;
[((q `1) `1),((q `2) `1)] in P by A1, Th10;
then consider x, y being set such that
A7: [((q `1) `1),((q `2) `1)] = [x,y] and
A8: x in A and
A9: y in B by RELSET_1:6;
consider a1, b1 being set such that
A10: q `1 = [a1,b1] by A1, Th10;
A11: b = [a2,b2] by A2, A6, MCART_1:7;
then A12: b `2 = t by A3, A6, ZFMISC_1:33;
A13: a = [a1,b1] by A2, A10, MCART_1:7;
then A14: a `2 = s by A3, A10, ZFMISC_1:33;
b `1 = y by A7, A6, A11, ZFMISC_1:33;
then A15: b in [:B,Y:] by A9, A5, A11, A12, MCART_1:11;
a `1 = x by A7, A10, A13, ZFMISC_1:33;
then a in [:A,X:] by A8, A4, A13, A14, MCART_1:11;
hence q in [:[:A,X:],[:B,Y:]:] by A2, A15, ZFMISC_1:def 2; :: thesis: verum

end;

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