pi-base
Theorem Suggestion: LOTS + extremally disconnected => discrete
As shown in {{mathse:4913523}} (https://math.stackexchange.com/q/4913523).
On the other hand, we can be inspired by the given answer to construct an example which is LOTS and sequentially discrete but not discrete. Please kindly check if everything goes well! :)
The example is $(\omega_1\times\mathbb{Z})\cup\{\infty\}$ with lexicographical order. Obviously enough, the space is Lindelöf (an open cover of $\infty$ leaves us with countably many points) but not hereditary Lindelöf (as $\omega_1\times\mathbb{Z}$ is uncountable discrete).
I don't follow why the order-convex nbhd must be a LOTS.
Yes, my bad! I have rewritten the proof and posted it in the Math SE link above. But still, nothing much in the original proof has to be changed :)
Is the example in the original post intended to be added to pi-base under this issue? Or can this issue be closed, since the suggested theorem has been added here https://topology.pi-base.org/theorems/T000539?
