Step * of Lemma es-le-loc

[es:EO]. ∀[e,e':E].  loc(e) loc(e') ∈ Id supposing e ≤loc e' 
BY
(Auto THEN -1 THEN Auto) }


Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    loc(e)  =  loc(e')  supposing  e  \mleq{}loc  e' 


By

(Auto  THEN  D  -1  THEN  Auto)




Home Index