feat: prove T597, hyperconnected with an isolated point gives a generic point

[kisonecat]

Adds T597: a hyperconnected space with an isolated point has a generic point.

If p is isolated then {p} is a nonempty open set, so hyperconnectedness makes every
nonempty open set meet {p} — that is, contain p. Hence every neighbourhood of every point
meets {p}, so closure {p} is the whole space and p is generic.

Closes #1028.