RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x)) by Th19;
hence ClNLin (rng x) is separable by Th25, Th26; :: thesis: verum