for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2
for a being Element of C1
for y being set holds
( y in f . a iff ex b being Element of C1 st
( [b,y] in Trace f & b c= a ) )