let f be Function of (bool X),(bool X); :: thesis: ( f is /\-preserving implies f is c=-monotone )
assume A1: f is /\-preserving ; :: thesis: f is c=-monotone
let A, B be Subset of X; :: according to ROUGHS_4:def 8 :: thesis: ( A c= B implies f . A c= f . B )
assume A c= B ; :: thesis: f . A c= f . B
then A /\ B = A by XBOOLE_1:28;
then (f . A) /\ (f . B) = f . A by A1;
hence f . A c= f . B by XBOOLE_1:17; :: thesis: verum