theorem Th92: :: TDLAT_2:93

for T being non empty TopSpace
for F being Subset-Family of T st F is domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )