let C1, C2 be Coherence_Space; :: thesis: for f being Function of C1,C2
for a being Element of C1
for y1, y2 being set st [a,y1] in graph f & [a,y2] in graph f holds
{y1,y2} in C2
let f be Function of C1,C2; :: thesis: for a being Element of C1
for y1, y2 being set st [a,y1] in graph f & [a,y2] in graph f holds
{y1,y2} in C2
let a be Element of C1; :: thesis: for y1, y2 being set st [a,y1] in graph f & [a,y2] in graph f holds
{y1,y2} in C2
let y1, y2 be set ; :: thesis: ( [a,y1] in graph f & [a,y2] in graph f implies {y1,y2} in C2 )
assume ( [a,y1] in graph f & [a,y2] in graph f ) ; :: thesis: {y1,y2} in C2
then ( y1 in f . a & y2 in f . a ) by Th24;
then {y1,y2} c= f . a by ZFMISC_1:32;
hence {y1,y2} in C2 by CLASSES1:def 1; :: thesis: verum