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 )
proof
let p be Element of L; :: according to QUANTAL1:def 10 :: thesis: p [= f . p
thus p [= f . p ; :: thesis: verum
end;
thus f is deflationary :: thesis: f is monotone
proof
let p be Element of L; :: according to QUANTAL1:def 11 :: thesis: f . p [= p
thus f . p [= p ; :: thesis: verum
end;
let p, q be Element of L; :: according to QUANTAL1:def 12 :: thesis: ( p [= q implies f . p [= f . q )
thus ( p [= q implies f . p [= f . q ) ; :: thesis: verum