theorem :: TDLAT_3:48

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 <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) )