let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is closed-domains-family holds
F is domains-family
let F be Subset-Family of T; :: thesis: ( F is closed-domains-family implies F is domains-family )
thus ( F is closed-domains-family implies F is domains-family ) :: thesis: verum
proof
assume F is closed-domains-family ; :: thesis: F is domains-family
then A1: F c= Closed_Domains_of T by Th71;
Closed_Domains_of T c= Domains_of T by TDLAT_1:31;
then F c= Domains_of T by A1;
hence F is domains-family by Th64; :: thesis: verum
end;