for C1, C2 being Coherence_Space holds union (C1 "/\" C2) = (union C1) U+ (union C2)