Piotr Pikul

I saw that **metrization theorem for locally orderable spaces** (2.12 in the article) would resolve few traits in pi-base: [Locally orderable](https://topology.pi-base.org/properties/P000120) + [G-delta diagonal](https://topology.pi-base.org/properties/P000106) + [Paracompact](https://topology.pi-base.org/properties/P000030) +[Hausdorff](https://topology.pi-base.org/properties/P000003) => [Metrizable](https://topology.pi-base.org/properties/P000053) All...

Actually we should probably add just > Locally orderable + $G_\delta$ diagonal $\Rightarrow$ Locally metrizable And a hereditarity (meta-property) to [G-delta diagonal](https://topology.pi-base.org/properties/P000106).

I guess we can close this. Possibly adding some new examples may be another issue.

This seems deeply related with **meta-properties** (see #1071), and implementation attempts should take into account whether we want to handle something more than just Kolmogorov quotients.

Some traits are redundant, e.g. P1, P13, P28, P43, P46, P139

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\\}$.

I would call it the **rational edge halfplane**. Or a **fringed carpet space** if aiming for something whimsy.

I see the theorem list on $\pi$-Base as a very supporting element. The automated deduction for "standard facts" provides often a ridiculously twisted path. And unless we want to introduce...