let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds
( F c= Domains_of T iff F is domains-family )
let F be Subset-Family of T; :: thesis: ( F c= Domains_of T iff F is domains-family )
thus ( F c= Domains_of T implies F is domains-family ) :: thesis: ( F is domains-family implies F c= Domains_of T )

proof

assume A1: F c= Domains_of T ; :: thesis: F is domains-family

now :: thesis: for A being Subset of T st A in F holds
A is condensed

let A be Subset of T; :: thesis: ( A in F implies A is condensed )
assume A in F ; :: thesis: A is condensed
then A in Domains_of T by A1;
then A in { P where P is Subset of T : P is condensed } by TDLAT_1:def 1;
then ex Q being Subset of T st
( Q = A & Q is condensed ) ;
hence A is condensed ; :: thesis: verum

end;

hence F is domains-family ; :: thesis: verum

end;

thus ( F is domains-family implies F c= Domains_of T ) :: thesis: verum

proof

assume A2: F is domains-family ; :: thesis: F c= Domains_of T
for X being object st X in F holds
X in Domains_of T

proof

let X be object ; :: thesis: ( X in F implies X in Domains_of T )
assume A3: X in F ; :: thesis: X in Domains_of T
then reconsider X0 = X as Subset of T ;
X0 is condensed by A2, A3;
then X0 in { P where P is Subset of T : P is condensed } ;
hence X in Domains_of T by TDLAT_1:def 1; :: thesis: verum

end;

hence F c= Domains_of T ; :: thesis: verum

end;