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,(Domains_Lattice Y)) = Cl (union F)
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,(Domains_Lattice Y)) = Cl (union F) )
assume F is domains-family ; :: thesis: for S being Subset of (Domains_Lattice Y) st S = F holds
"\/" (S,(Domains_Lattice Y)) = Cl (union F)
then F c= Domains_of Y by TDLAT_2:65;
then F c= Closed_Domains_of Y by Th39;
then A1: F is closed-domains-family by TDLAT_2:72;
let S be Subset of (Domains_Lattice Y); :: thesis: ( S = F implies "\/" (S,(Domains_Lattice Y)) = Cl (union F) )
reconsider P = S as Subset of (Closed_Domains_Lattice Y) by Th41;
assume A2: S = F ; :: thesis: "\/" (S,(Domains_Lattice Y)) = Cl (union F)
thus "\/" (S,(Domains_Lattice Y)) = "\/" (P,(Closed_Domains_Lattice Y)) by Th41
.= Cl (union F) by A1, A2, TDLAT_2:100 ; :: thesis: verum