theorem Th10: :: YELLOW_3:10

for P, R being Relation
for x being object 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 object st x = [a,b] & ex c, d being object st x `1 = [c,d] & ex e, f being object st x `2 = [e,f] ) )