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 )

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

( 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 A2:
f is V224()
; :: thesis: f is monotone
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;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

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