Un . n c= bool the carrier of T ;
hence Un . n is Subset-Family of T ; :: thesis: verum