for C1, C2 being Coherence_Space
for x being set holds
( x in C1 [*] C2 iff ex a being Element of C1 ex b being Element of C2 st x c= [:a,b:] )