:: deftheorem Def3 defines [^ PCS_0:def 3 :
for R1, R2, S1, S2 being non empty 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 r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in b₇ iff ( [r1,r2] in R or [s1,s2] in S ) ) );