theorem Th10: :: QUANTAL1:10

for L being complete Lattice
for j being UnOp of L st j is monotone holds
( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) )