:: deftheorem defines \/-distributive QUANTAL1:def 13 :
for L being non empty LattStr
for IT being UnOp of L holds
( IT is \/-distributive iff for X being Subset of L holds IT . ("\/" X) [= "\/" ( { (IT . a) where a is Element of L : a in X } ,L) );