let C1, C2 be Coherence_Space; :: thesis: for f being cap-distributive Function of C1,C2
for x1, x2 being set st {x1,x2} in C1 holds
for y being set st [x1,y] in LinTrace f & [x2,y] in LinTrace f holds
x1 = x2
let f be cap-distributive Function of C1,C2; :: thesis: for x1, x2 being set st {x1,x2} in C1 holds
for y being set st [x1,y] in LinTrace f & [x2,y] in LinTrace f holds
x1 = x2
A1: dom f = C1 by FUNCT_2:def 1;
let a1, a2 be set ; :: thesis: ( {a1,a2} in C1 implies for y being set st [a1,y] in LinTrace f & [a2,y] in LinTrace f holds
a1 = a2 )
set a = {a1,a2};
assume A2: {a1,a2} in C1 ; :: thesis: for y being set st [a1,y] in LinTrace f & [a2,y] in LinTrace f holds
a1 = a2
A3: {a1,a2} = {a1} \/ {a2} by ENUMSET1:41;
let y be set ; :: thesis: ( [a1,y] in LinTrace f & [a2,y] in LinTrace f implies a1 = a2 )
assume ( [a1,y] in LinTrace f & [a2,y] in LinTrace f ) ; :: thesis: a1 = a2
then ( [{a1},y] in Trace f & [{a2},y] in Trace f & {a1} in C1 & {a2} in C1 ) by A1, Th51, Th53;
then {a1} = {a2} by A2, A3, Th36;
hence a1 = a2 by ZFMISC_1:6; :: thesis: verum