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