theorem Th54: :: COHSP_1:54

for C1, C2 being Coherence_Space
for f being cap-distributive Function of C1,C2
for x1, x2 being set st {x1,x2} in C1 holds
for y being object st [x1,y] in LinTrace f & [x2,y] in LinTrace f holds
x1 = x2