let C be Coherence_Space; :: thesis: C is d.union-closed
let A be Subset of C; :: according to COHSP_1:def 6 :: thesis: ( A is c=directed implies union A in C )
thus ( A is c=directed implies union A in C ) by Th15; :: thesis: verum