reconsider f = id the carrier of L as UnOp of L ;

take f ; :: thesis: ( f is inflationary & f is deflationary & f is monotone )

thus f is inflationary :: thesis: ( f is deflationary & f is monotone )

thus ( p [= q implies f . p [= f . q ) ; :: thesis: verum

take f ; :: thesis: ( f is inflationary & f is deflationary & f is monotone )

thus f is inflationary :: thesis: ( f is deflationary & f is monotone )

proof

thus
f is deflationary
:: thesis: f is monotone
let p be Element of L; :: according to QUANTAL1:def 10 :: thesis: p [= f . p

thus p [= f . p ; :: thesis: verum

end;thus p [= f . p ; :: thesis: verum

proof

let p, q be Element of L; :: according to QUANTAL1:def 12 :: thesis: ( p [= q implies f . p [= f . q )
let p be Element of L; :: according to QUANTAL1:def 11 :: thesis: f . p [= p

thus f . p [= p ; :: thesis: verum

end;thus f . p [= p ; :: thesis: verum

thus ( p [= q implies f . p [= f . q ) ; :: thesis: verum