---

Step * of Lemma geo-left-transitivity

∀g:OrientedPlane. ∀t,s,p,q,r:Point.
  (p leftof ts ⇒ q leftof ts ⇒ r leftof ts ⇒ q leftof tp ⇒ r leftof tq ⇒ (¬r leftof pt))
BY
{ (InstLemma `left-transitivity` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}t,s,p,q,r:Point.
    (p  leftof  ts  {}\mRightarrow{}  q  leftof  ts  {}\mRightarrow{}  r  leftof  ts  {}\mRightarrow{}  q  leftof  tp  {}\mRightarrow{}  r  leftof  tq  {}\mRightarrow{}  (\mneg{}r  leftof  pt))


By

---

Latex:
(InstLemma  `left-transitivity`  []  THEN  Trivial)

---

Home Index