theorem :: LATTICE3:48

for C being complete Lattice
for X being set st X c= bool the carrier of C holds
"\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C)