---

Step * of Lemma geo-between-implies-out3

∀e:BasicGeometry. ∀p,a,b,c:Point.  (p-b-a ⇒ p-c-a ⇒ out(p bc))
BY
{ ((Auto THEN RepeatFor 2 ((D -2 THEN FLemma `geo-between-out` [-3] THEN Auto)))
   THEN InstLemma `geo-out_transitivity` [⌜e⌝;⌜p⌝;⌜b⌝;⌜a⌝;⌜c⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,a,b,c:Point.    (p-b-a  {}\mRightarrow{}  p-c-a  {}\mRightarrow{}  out(p  bc))


By

---

Latex:
((Auto  THEN  RepeatFor  2  ((D  -2  THEN  FLemma  `geo-between-out`  [-3]  THEN  Auto)))
  THEN  InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index