{} T is condensed by Th14;
then {} T in { A where A is Subset of T : A is condensed } ;
hence not Domains_of T is empty ; :: thesis: verum