for C1, C2 being Coherence_Space
for A being set st ( for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f ) holds
ex f being U-stable Function of C1,C2 st union A = Trace f