consider C being Coherence_Space;
take C ; :: thesis: ( C is multiplicative & C is d.union-closed )
thus ( C is multiplicative & C is d.union-closed ) ; :: thesis: verum