let C1, C2 be Coherence_Space; :: thesis: for f being c=-monotone Function of C1,C2
for a1, a2 being set st a1 \/ a2 in C1 holds
for y1, y2 being object st [a1,y1] in Trace f & [a2,y2] in Trace f holds
{y1,y2} in C2
let f be c=-monotone Function of C1,C2; :: thesis: for a1, a2 being set st a1 \/ a2 in C1 holds
for y1, y2 being object st [a1,y1] in Trace f & [a2,y2] in Trace 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 object st [a1,y1] in Trace f & [a2,y2] in Trace f holds
{y1,y2} in C2 )
set a = a1 \/ a2;
assume a1 \/ a2 in C1 ; :: thesis: for y1, y2 being object st [a1,y1] in Trace f & [a2,y2] in Trace f holds
{y1,y2} in C2
then reconsider a = a1 \/ a2 as Element of C1 ;
A2: a2 c= a by XBOOLE_1:7;
then a2 in C1 by CLASSES1:def 1;
then A3: f . a2 c= f . a by A1, A2, Def11;
let y1, y2 be object ; :: thesis: ( [a1,y1] in Trace f & [a2,y2] in Trace f implies {y1,y2} in C2 )
assume ( [a1,y1] in Trace f & [a2,y2] in Trace f ) ; :: thesis: {y1,y2} in C2
then A4: ( y1 in f . a1 & y2 in f . a2 ) by Th31;
A5: a1 c= a by XBOOLE_1:7;
then a1 in C1 by CLASSES1:def 1;
then f . a1 c= f . a by A1, A5, Def11;
then {y1,y2} c= f . a by A3, A4, ZFMISC_1:32;
hence {y1,y2} in C2 by CLASSES1:def 1; :: thesis: verum