let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds
( F c= Closed_Domains_of T iff F is closed-domains-family )
let F be Subset-Family of T; :: thesis: ( F c= Closed_Domains_of T iff F is closed-domains-family )
thus ( F c= Closed_Domains_of T implies F is closed-domains-family ) :: thesis: ( F is closed-domains-family implies F c= Closed_Domains_of T )
proof
assume A1: F c= Closed_Domains_of T ; :: thesis: F is closed-domains-family
now :: thesis: for A being Subset of T st A in F holds
A is closed_condensed
let A be Subset of T; :: thesis: ( A in F implies A is closed_condensed )
assume A in F ; :: thesis: A is closed_condensed
then A in Closed_Domains_of T by A1;
then A in { P where P is Subset of T : P is closed_condensed } by TDLAT_1:def 5;
then ex Q being Subset of T st
( Q = A & Q is closed_condensed ) ;
hence A is closed_condensed ; :: thesis: verum
end;
hence F is closed-domains-family ; :: thesis: verum
end;
thus ( F is closed-domains-family implies F c= Closed_Domains_of T ) :: thesis: verum
proof
assume A2: F is closed-domains-family ; :: thesis: F c= Closed_Domains_of T
for X being object st X in F holds
X in Closed_Domains_of T
proof
let X be object ; :: thesis: ( X in F implies X in Closed_Domains_of T )
assume A3: X in F ; :: thesis: X in Closed_Domains_of T
then reconsider X0 = X as Subset of T ;
X0 is closed_condensed by A2, A3;
then X0 in { P where P is Subset of T : P is closed_condensed } ;
hence X in Closed_Domains_of T by TDLAT_1:def 5; :: thesis: verum
end;
hence F c= Closed_Domains_of T ; :: thesis: verum
end;