Novak space is extremally disconnected

[Moniker1998]

#1055

[prabau]

The proof that the extremally disconnected property is preserved by dense sets is really not hard. But we can change the Engelking reference to something more explicit for the benefit of pi-base users. Let me make a suggestion below.

[prabau]

see #1202.
We may instead remove all references to that fact here and add a meta-property on the page for the extremally disconnected property. So we would have a common reference available for all spaces that need it.

[prabau]

As for the Novak space itself, I have not taken time to read the description yet, so I cannot comment on it at this point. If anyone else wants to review this, please feel free.

[pzjp]

I would add to the definition of the Novak space a reference to item 1 in Counterexamples... to justify the existence of the family $\{P_A:A\in F\}$.

[Moniker1998]

@pzjp The definition of Novak space needs a whole revamp, but this is for another PR #1218