{} T is open_condensed by Th20;
then {} T in { A where A is Subset of T : A is open_condensed } ;
hence not Open_Domains_of T is empty ; :: thesis: verum