let Y be non empty extremally_disconnected TopSpace; :: thesis: for F being Subset-Family of st F is domains-family holds
for S being Subset of 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 ; :: thesis: ( F is domains-family implies for S being Subset of 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 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 Th44;
then A2: F is open-domains-family by TDLAT_2:79;
let S be Subset of ; :: 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 Th46;
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