for C being Coherence_Space
for A being c=directed Subset of C holds union A in C