for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2
for X being Subset of (Trace f) ex g being U-stable Function of C1,C2 st Trace g = X