let f be Function; :: thesis: ( f is d.union-distributive implies f is c=-monotone )
assume A1: for A being Subset of (dom f) st A is c=directed & union A in dom f holds
f . (union A) = union (f .: A) ; :: according to COHSP_1:def 10 :: thesis: f is c=-monotone
let a, b be set ; :: according to COHSP_1:def 11 :: thesis: ( a in dom f & b in dom f & a c= b implies f . a c= f . b )
assume that
A2: a in dom f and
A3: b in dom f and
A4: a c= b ; :: thesis: f . a c= f . b
reconsider A = {a,b} as Subset of (dom f) by A2, A3, ZFMISC_1:32;
A5: A is c=directed

proof

let Y be finite Subset of A; :: according to COHSP_1:def 4 :: thesis: ex a being set st
( union Y c= a & a in A )
take b ; :: thesis: ( union Y c= b & b in A )
union Y c= union A by ZFMISC_1:77;
then union Y c= a \/ b by ZFMISC_1:75;
hence ( union Y c= b & b in A ) by A4, TARSKI:def 2, XBOOLE_1:12; :: thesis: verum

end;

a in A by TARSKI:def 2;
then A6: f . a in f .: A by FUNCT_1:def 6;
union A = a \/ b by ZFMISC_1:75
.= b by A4, XBOOLE_1:12 ;
then union (f .: A) = f . b by A1, A3, A5;
hence f . a c= f . b by A6, ZFMISC_1:74; :: thesis: verum