let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is open-domains-family holds
for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))
let F be Subset-Family of T; :: thesis: ( F is open-domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) )
A1: Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19;
assume A2: F is open-domains-family ; :: thesis: for X being Subset of (Domains_Lattice T) st X = F holds
"\/" (X,(Domains_Lattice T)) = Int (Cl (union F))
then union F is open by Th80, TOPS_2:19;
then union F c= Int (Cl (union F)) by A1, TOPS_1:23;
then A3: (union F) \/ (Int (Cl (union F))) = Int (Cl (union F)) by XBOOLE_1:12;
let X be Subset of (Domains_Lattice T); :: thesis: ( X = F implies "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) )
assume X = F ; :: thesis: "\/" (X,(Domains_Lattice T)) = Int (Cl (union F))
hence "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) by A2, A3, Th79, Th91; :: thesis: verum