let A be non empty set ; :: thesis: for f being UnOp of (BooleLatt A) holds
( f is monotone iff f is c=-monotone )
let f be UnOp of (BooleLatt A); :: thesis: ( f is monotone iff f is c=-monotone )
thus ( f is monotone implies f is c=-monotone ) :: thesis: ( f is c=-monotone implies f is monotone )

proof

assume A1: f is monotone ; :: thesis: f is c=-monotone
let x, y be Element of (BooleLatt A); :: according to KNASTER:def 1 :: thesis: ( x c= y implies f . x c= f . y )
assume x c= y ; :: thesis: f . x c= f . y
then x [= y by LATTICE3:2;
then f . x [= f . y by A1;
hence f . x c= f . y by LATTICE3:2; :: thesis: verum

end;

assume A2: f is c=-monotone ; :: thesis: f is monotone
let p, q be Element of (BooleLatt A); :: according to QUANTAL1:def 12 :: thesis: ( not p [= q or f . p [= f . q )
assume p [= q ; :: thesis: f . p [= f . q
then p c= q by LATTICE3:2;
then f . p c= f . q by A2;
hence f . p [= f . q by LATTICE3:2; :: thesis: verum