let P, R be Relation; :: thesis: for x being set holds
( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )
let x be set ; :: thesis: ( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )

hereby :: thesis: ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] implies x in ["P,R"] )

assume A1: x in ["P,R"] ; :: thesis: ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
then consider y, z being set such that
A2: x = [y,z] by RELAT_1:def 1;
consider p, q, s, t being set such that
A3: y = [p,q] and
A4: z = [s,t] and
A5: ( [p,s] in P & [q,t] in R ) by A1, A2, Def1;
( (x `1) `1 = p & (x `1) `2 = q ) by A2, A3, A4, Lm1;
hence ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R ) by A2, A3, A4, A5, Lm1; :: thesis: ( ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
thus ex a, b being set st x = [a,b] by A2; :: thesis: ( ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
thus ex c, d being set st x `1 = [c,d] by A2, A3, MCART_1:7; :: thesis: ex e, f being set st x `2 = [e,f]
thus ex e, f being set st x `2 = [e,f] by A2, A4, MCART_1:7; :: thesis: verum

end;

assume that
A6: [((x `1) `1),((x `2) `1)] in P and
A7: [((x `1) `2),((x `2) `2)] in R and
A8: ex a, b being set st x = [a,b] and
A9: ex c, d being set st x `1 = [c,d] and
A10: ex e, f being set st x `2 = [e,f] ; :: thesis: x in ["P,R"]
consider c, d being set such that
A11: x `1 = [c,d] by A9;
consider e, f being set such that
A12: x `2 = [e,f] by A10;
[c,((x `2) `1)] in P by A6, A11, MCART_1:7;
then A13: [c,e] in P by A12, MCART_1:7;
consider a, b being set such that
A14: x = [a,b] by A8;
[d,((x `2) `2)] in R by A7, A11, MCART_1:7;
then A15: [d,f] in R by A12, MCART_1:7;
A16: b = [e,f] by A14, A12, MCART_1:7;
a = [c,d] by A14, A11, MCART_1:7;
hence x in ["P,R"] by A14, A16, A13, A15, Def1; :: thesis: verum