Step * of Lemma es-causl_weakening

es:EO. ∀a,b:E.  ((a <loc b)  (a < b))
BY
(Auto THEN (InstESAxiom ⌜es⌝ [] 10)⋅ THEN (BHyp (-1)) THEN Auto) }


Latex:


Latex:
\mforall{}es:EO.  \mforall{}a,b:E.    ((a  <loc  b)  {}\mRightarrow{}  (a  <  b))


By


Latex:
(Auto  THEN  (InstESAxiom  \mkleeneopen{}es\mkleeneclose{}  []  10)\mcdot{}  THEN  (BHyp  (-1))  THEN  Auto)




Home Index