theorem :: TDLAT_2:100

for T being non empty TopSpace
for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Closed_Domains_Lattice T) st X = F holds
"\/" (X,(Closed_Domains_Lattice T)) = Cl (union F)