Theorem DenselyOrdered.subsingleton_of_discreteTopology

feat: if the order topology for a dense linear ordering is discrete, the space has at most one point (#30856) …