let T be 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 <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )
let F be Subset-Family of T; ( F is closed-domains-family implies for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) )
assume A1:
F is closed-domains-family
; for X being Subset of (Closed_Domains_Lattice T) st X = F holds
( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )
let X be Subset of (Closed_Domains_Lattice T); ( X = F implies ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) )
assume A2:
X = F
; ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) )
thus
( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) )
( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T )
thus
( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T )
verum