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