3 new alpha1 theorems

[felixpernegger]

(I know I said I wouldnt open new PRs for now, but I really like the results here.)

This implements the missing theorems from this comment.

This gives two more traits, but very plausible many more (since for 14/17 remaining spaces either W-space, P-space or well based is still unknown).

We cant use explore to refer the the theorems used in the proof, otherwise the explore will just refer to the theorem itself, I tested this.
(Except for some reason for the third one it works as intended; to keep consistent and more stable to potential changes to pibase, lets keep it like it is however)

This PR has medium priority!

[felixpernegger]

I want to emphasise, that we have had great progress on the alpha_i properties. When I joined in November, there was pretty much only First countable => alpha_1, but now we are getting very close to actually completing the properties. (Despite still having no nonterminal pi-base theorems about them!) :)

[prabau]

Suggested change

	Utilising the metaproperties of {P210} and {P147}, we may assume that $X$ is {P57}. But then the assertion follows from {T238}, {T748}, {T894} and {T285}.
	To prove the result it is enough to show every countable subspace of $X$ is {P210}.
	Note that each subspace of $X$ is also {P147}.
	So wlog we may assume $X$ is {P57}, and hence {P28}
	[(Explore)](https://topology.pi-base.org/spaces?q=Countable%2BP-space%2B%7EFirst+countable).
	And {T748}.