:: deftheorem defines deflationary QUANTAL1:def 11 :
for L being non empty LattStr
for IT being UnOp of L holds
( IT is deflationary iff for p being Element of L holds IT . p [= p );