for C1, C2 being Coherence_Space
for f being Function of C1,C2
for a being Element of C1
for y1, y2 being set st [a,y1] in graph f & [a,y2] in graph f holds
{y1,y2} in C2