∀es:EO. ∀a,b:E.  ((a < b) 
 a c≤ b)
{ Auto }
1. es : EO@i'
2. a : E@i
3. b : E@i
4. (a < b)@i
⊢ a c≤ b