let C1, C2 be Coherence_Space; :: thesis: for f being c=-monotone Function of C1,C2
for x1, x2 being set st {x1,x2} in C1 holds
for y1, y2 being set st [x1,y1] in LinTrace f & [x2,y2] in LinTrace f holds
{y1,y2} in C2
let f be c=-monotone Function of C1,C2; :: thesis: for x1, x2 being set st {x1,x2} in C1 holds
for y1, y2 being set st [x1,y1] in LinTrace f & [x2,y2] in LinTrace f holds
{y1,y2} in C2
A1: dom f = C1 by FUNCT_2:def 1;
let a1, a2 be set ; :: thesis: ( {a1,a2} in C1 implies for y1, y2 being set st [a1,y1] in LinTrace f & [a2,y2] in LinTrace f holds
{y1,y2} in C2 )
assume {a1,a2} in C1 ; :: thesis: for y1, y2 being set st [a1,y1] in LinTrace f & [a2,y2] in LinTrace f holds
{y1,y2} in C2
then reconsider a = {a1,a2} as Element of C1 ;
A2: ( {a1} c= a & {a2} c= a ) by ZFMISC_1:12;
then ( {a1} in C1 & {a2} in C1 ) by CLASSES1:def 1;
then A3: ( f . {a1} c= f . a & f . {a2} c= f . a ) by A1, A2, Def12;
let y1, y2 be set ; :: thesis: ( [a1,y1] in LinTrace f & [a2,y2] in LinTrace f implies {y1,y2} in C2 )
assume ( [a1,y1] in LinTrace f & [a2,y2] in LinTrace f ) ; :: thesis: {y1,y2} in C2
then ( y1 in f . {a1} & y2 in f . {a2} ) by Th53;
then {y1,y2} c= f . a by A3, ZFMISC_1:38;
hence {y1,y2} in C2 by CLASSES1:def 1; :: thesis: verum