Theorem Suggestion
If a space is:
then it is paracompact P30.
Proof/References
Theorem 3.2 in Paracompactness in ordered spaces by Engelking and Lutzer
(note Dieudonne complete is not added yet)
@pzjp perhaps you could take a look after #1426 is done