:: deftheorem Def2 defines [^ PCS_0:def 2 :
for R1, R2, S1, S2 being set
for R being Relation of R1,R2
for S being Relation of S1,S2
for b₇ being Relation of [:R1,S1:],[:R2,S2:] holds
( b₇ = [^R,S^] iff for x, y being object holds
( [x,y] in b₇ iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) );