let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is open-domains-family holds
F is domains-family
let F be Subset-Family of T; :: thesis: ( F is open-domains-family implies F is domains-family )
thus ( F is open-domains-family implies F is domains-family ) :: thesis: verum

proof

assume F is open-domains-family ; :: thesis: F is domains-family
then A1: F c= Open_Domains_of T by Th78;
Open_Domains_of T c= Domains_of T by TDLAT_1:35;
then F c= Domains_of T by A1;
hence F is domains-family by Th64; :: thesis: verum

end;