theorem :: LATTICE3:55

for D being non empty set
for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds
ex L being strict complete Lattice st
( the carrier of L = D & ( for X being Subset of L holds "\/" X = f . X ) ) by Lm3;