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 = B by XBOOLE_1:12;
then (f . A) \/ (f . B) = f . B by A1;
hence f . A c= f . B by XBOOLE_1:7; :: thesis: verum