for C1, C2 being Coherence_Space
for a being Element of C1 [*] C2 holds
( proj1 a in C1 & proj2 a in C2 & a c= [:(proj1 a),(proj2 a):] )