---

Step * of Lemma geo-between-outer-trans2-cpy

No Annotations
∀e:EuclideanPlane. ∀[a,b,c,d:Point].  (B(abd)) supposing (B(bcd) and B(abc) and b # c)
BY
{ ((Auto THEN (Assert c # b BY EAuto 1))
   THEN InstLemma `geo-between-outer-trans-cpy` [⌜e⌝;⌜d⌝;⌜c⌝;⌜b⌝;⌜a⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c,d:Point].    (B(abd))  supposing  (B(bcd)  and  B(abc)  and  b  \#  c)


By

---

Latex:
((Auto  THEN  (Assert  c  \#  b  BY  EAuto  1))
  THEN  InstLemma  `geo-between-outer-trans-cpy`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index