theorem Th35: :: COHSP_1:35

for C1, C2 being Coherence_Space
for f being cap-distributive Function of C1,C2
for a1, a2 being set st a1 \/ a2 in C1 holds
for y being object st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2