∀r,u:Top.  (r ∈ (-∞, u) ~ r < u)
{ (UnivCD THENA Auto) }
1. r : Top@i
2. u : Top@i
⊢ r ∈ (-∞, u) ~ r < u