let Y be 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 ) )
let F be Subset-Family of Y; ( F is domains-family implies 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 ) ) )
assume A1:
F is domains-family
; 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 ) )
then
F c= Domains_of Y
by TDLAT_2:65;
then
F c= Open_Domains_of Y
by Th42;
then A2:
F is open-domains-family
by TDLAT_2:79;
let S be Subset of (Domains_Lattice Y); ( S = F implies ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) )
assume A3:
S = F
; ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) )
Domains_Lattice Y = Open_Domains_Lattice Y
by Th44;
hence
( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) )
by A2, A3, TDLAT_2:110; ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y )
assume
S = {}
; "/\" (S,(Domains_Lattice Y)) = [#] Y
hence
"/\" (S,(Domains_Lattice Y)) = [#] Y
by A1, A3, TDLAT_2:93; verum