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

proof

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

now

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

end;

hence F is open-domains-family by Def4; :: thesis: verum

end;

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

proof

assume A2: F is open-domains-family ; :: thesis: F c= Open_Domains_of T
for X being set st X in F holds
X in Open_Domains_of T

proof

let X be set ; :: thesis: ( X in F implies X in Open_Domains_of T )
assume A3: X in F ; :: thesis: X in Open_Domains_of T
then reconsider X0 = X as Subset of ;
X0 is open_condensed by A2, A3, Def4;
then X0 in { P where P is Subset of : P is open_condensed } ;
hence X in Open_Domains_of T by TDLAT_1:def 9; :: thesis: verum

end;

hence F c= Open_Domains_of T by TARSKI:def 3; :: thesis: verum

end;