let A be non empty set ; :: thesis: for f being UnOp of (BooleLatt A) holds
( f is monotone iff f is V224() )
let f be UnOp of (BooleLatt A); :: thesis: ( f is monotone iff f is V224() )
thus ( f is monotone implies f is V224() ) :: thesis: ( f is V224() implies f is monotone )
proof
assume A1: f is monotone ; :: thesis: f is V224()
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 V224() ; :: 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