Some trait cleanup for Sphere S169

[prabau]

Cleaned up some of the redundant traits for Sphere S169: homogeneous and empty.
There remains two redundant traits:

• contractible = F (I would like to keep this one, as the current justification is instructive, and relying on Poincare duality (T685) really seems too much)
• embeddable into Euclidean space (the current justification is so short and obvious so seems worth keeping. But that could be debated.)

Also added missing newlines to the files added in #1797 (@artemetra fyi)