Hereditary traits for Converging sequence of non-Hausdorff spaces (S000186)

[felixpernegger]

Traits automatically deduced by tracking subspaces for Converging sequence of non-Hausdorff spaces (S000186). This PR was created with the help of Claude Code.

[GeoffreySangston]

The PR looks good. Is the goal here to remove the redundant ones as well? I.e. the system marks P210 through P213 with asterisks (redundant). So I guess we only want to keep P214?

[felixpernegger]

@GeoffreySangston the subspace deduction gives many traits, but those may make old traits and other new traits redundant (i.e. subspace deduction gives P2 and P1, but obvioulsy we dont need to add P1 since its implied by P2).
For these PRs I only removed (not included) new traits that would already be redundant by other new traits.

It would be very easy to just remove all redundant traits, but per discussion at #1629 and simplicity didnt remove old traits that may become redundant (or already were redundant in the first place).
It's probably better to do this seperately.

[felixpernegger]

@prabau can you take a quick look at this? The subspace relation (to which I changed now) is in the definition and this is the last one remaning of the subspace PRs

[prabau]

Sorry, did not get the time. Will look at it tomorrow for sure.