theorem :: TDLAT_3:47
for Y being non empty extremally_disconnected TopSpace
for F being Subset-Family of Y st F is domains-family holds
for S being Subset of (Domains_Lattice Y) st S = F holds
"\/" (S,(Domains_Lattice Y)) = Cl (union F)