theorem :: COHSP_1:27

for C1, C2 being Coherence_Space
for f being c=-monotone Function of C1,C2
for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in graph f & [b,y2] in graph f holds
{y1,y2} in C2