let C1, C2 be Coherence_Space; :: thesis: for f being c=-monotone Function of C1,C2
for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in graph f & [b,y2] in graph f holds
{y1,y2} in C2
let f be c=-monotone Function of C1,C2; :: thesis: for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in graph f & [b,y2] in graph f holds
{y1,y2} in C2
let a, b be Element of C1; :: thesis: ( a \/ b in C1 implies for y1, y2 being set st [a,y1] in graph f & [b,y2] in graph f holds
{y1,y2} in C2 )
assume A1: a \/ b in C1 ; :: thesis: for y1, y2 being set st [a,y1] in graph f & [b,y2] in graph f holds
{y1,y2} in C2
let y1, y2 be set ; :: thesis: ( [a,y1] in graph f & [b,y2] in graph f implies {y1,y2} in C2 )
assume A2: ( [a,y1] in graph f & [b,y2] in graph f ) ; :: thesis: {y1,y2} in C2
then ( a is finite & b is finite ) by Th24;
then reconsider c = a \/ b as finite Element of C1 by A1;
dom f = C1 by FUNCT_2:def 1;
then ( [c,y1] in graph f & [c,y2] in graph f ) by A2, Th25, XBOOLE_1:7;
hence {y1,y2} in C2 by Th26; :: thesis: verum