let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is closed-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
let F be Subset-Family of T; :: thesis: ( F is closed-domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) )
A1: Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16;
assume A2: F is closed-domains-family ; :: thesis: for X being Subset of (Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
then A3: F is domains-family by Th72;
let X be Subset of (Domains_Lattice T); :: thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) )
assume A4: X = F ; :: thesis: ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) )
meet F is closed by A2, Th73, TOPS_2:22;
then Cl (Int (meet F)) c= meet F by A1, PRE_TOPC:22;
then (meet F) /\ (Cl (Int (meet F))) = Cl (Int (meet F)) by XBOOLE_1:28;
hence ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) by A3, A4, Th92; :: thesis: ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T )
thus ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) by A3, A4, Th92; :: thesis: verum