set C = the Coherence_Space;
take the Coherence_Space ; :: thesis: ( the Coherence_Space is multiplicative & the Coherence_Space is d.union-closed )
thus ( the Coherence_Space is multiplicative & the Coherence_Space is d.union-closed ) ; :: thesis: verum