let Y be non empty extremally_disconnected TopSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( S = F implies ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) )
assume A3: S = F ; :: thesis: ( ( 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; :: thesis: ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y )
assume S = {} ; :: thesis: "/\" (S,(Domains_Lattice Y)) = [#] Y
hence "/\" (S,(Domains_Lattice Y)) = [#] Y by A1, A3, TDLAT_2:93; :: thesis: verum