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