∀ (α : Type u) [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] [SecondCountableTopology α],
  ∃ c, c.Countable ∧ ts = TopologicalSpace.generateFrom {s | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a}