let T be TopSpace; :: thesis: Closed_Domains_of T c= Domains_of T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Closed_Domains_of T or x in Domains_of T )
assume x in Closed_Domains_of T ; :: thesis: x in Domains_of T
then x in { A where A is Subset of T : A is closed_condensed } ;
then consider A1 being Subset of T such that
A1: ( x = A1 & A1 is closed_condensed ) ;
A1 is condensed by A1, TOPS_1:66;
then x in { A where A is Subset of T : A is condensed } by A1;
hence x in Domains_of T ; :: thesis: verum