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 11 :: thesis: f is c=-monotone
let a, b be set ; :: according to COHSP_1:def 12 :: thesis: ( a in dom f & b in dom f & a c= b implies f . a c= f . b )
assume A2: ( a in dom f & b in dom f & a c= b ) ; :: thesis: f . a c= f . b
then reconsider A = {a,b} as Subset of (dom f) by ZFMISC_1:38;
A3: union A = a \/ b by ZFMISC_1:93
.= b by A2, XBOOLE_1:12 ;
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:95;
then union Y c= a \/ b by ZFMISC_1:93;
hence ( union Y c= b & b in A ) by A2, TARSKI:def 2, XBOOLE_1:12; :: thesis: verum

end;

then A4: union (f .: A) = f . b by A1, A2, A3;
a in A by TARSKI:def 2;
then f . a in f .: A by FUNCT_1:def 12;
hence f . a c= f . b by A4, ZFMISC_1:92; :: thesis: verum