Continuing real TVS: Singleton and large indiscrete spaces have real TVS topologies

[GeoffreySangston]

Adds two more basic theorems.

(Brain slipped typing the commit message just now.)

[prabau]

T882: I was asking myself about the other approach, which is to add TVS as a trait for the Singleton space. Right now, all the other traits for the singleton are derived from the same two asserted traits (not multiple points + not empty). Mostly deriving all the other traits via discrete + indiscrete + not empty. But the various theorems being used for that are kind of useful in their own right (sometimes via the contrapositive).

But the proposed T882 does not seem like it would be helpful for other purposes. So wouldn't using a direct trait be equally good or better?

I take that back: Even if T882 does not seem very useful, it's fine to have it. So that a query like
π-Base, Search for ~Has multiple points + ~Empty + ~TVS
would return that it's impossible to satisfy.

Note: once we add the Euclidean property, this will be changed to assert Euclidean.