---

Step * of Lemma es-causle_antisymmetry

∀[es:EO]. ∀[a,b:E].  (a = b ∈ E) supposing (b c≤ a and a c≤ b)
BY
{ (Auto THEN (D -2 THEN Auto) THEN D -1 THEN Auto THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[a,b:E].    (a  =  b)  supposing  (b  c\mleq{}  a  and  a  c\mleq{}  b)


By

(Auto  THEN  (D  -2  THEN  Auto)  THEN  D  -1  THEN  Auto  THEN  Auto)

---

Home Index