let C1, C2 be Coherence_Space; :: thesis: for f being cap-distributive Function of C1,C2
for a1, a2 being set st a1 \/ a2 in C1 holds
for y being set st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2
let f be cap-distributive Function of C1,C2; :: thesis: for a1, a2 being set st a1 \/ a2 in C1 holds
for y being set st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2
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 Trace f & [a2,y] in Trace f holds
a1 = a2 )
set a = a1 \/ a2;
assume A2: a1 \/ a2 in C1 ; :: thesis: for y being set st [a1,y] in Trace f & [a2,y] in Trace f holds
a1 = a2
( a1 c= a1 \/ a2 & a2 c= a1 \/ a2 ) by XBOOLE_1:7;
then A3: ( a1 in C1 & a2 in C1 ) by A2, CLASSES1:def 1;
then reconsider b = a1 /\ a2 as Element of C1 by FINSUB_1:def 2;
b in C1 ;
then A4: C1 includes_lattice_of a1,a2 by A2, A3, Th17;
let y be set ; :: thesis: ( [a1,y] in Trace f & [a2,y] in Trace f implies a1 = a2 )
assume A5: ( [a1,y] in Trace f & [a2,y] in Trace f ) ; :: thesis: a1 = a2
then ( y in f . a1 & y in f . a2 ) by Th32;
then y in (f . a1) /\ (f . a2) by XBOOLE_0:def 4;
then ( y in f . b & b c= a1 & b c= a2 ) by A1, A4, Def13, XBOOLE_1:17;
then ( b = a1 & b = a2 ) by A1, A5, Th32;
hence a1 = a2 ; :: thesis: verum