---

Step * 1 of Lemma left-between-triangle


1. e : EuclideanPlane
2. a : Point
3. x : Point
4. y : Point
5. p : Point
6. a leftof xy
7. x-p-a
⊢ a leftof py
BY
{ ((Assert a # xy BY
          (Unfold `geo-lsep` 0 THEN Auto))
   THEN (Assert p leftof xy BY
               (InstLemma `left-convex2` [⌜e⌝;⌜x⌝;⌜y⌝;⌜a⌝;⌜p⌝]⋅ THEN Auto))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. x : Point
4. y : Point
5. p : Point
6. a leftof xy
7. x-p-a
8. a # xy
9. p leftof xy
⊢ a leftof py

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  x  :  Point
4.  y  :  Point
5.  p  :  Point
6.  a  leftof  xy
7.  x-p-a
\mvdash{}  a  leftof  py


By

---

Latex:
((Assert  a  \#  xy  BY
                (Unfold  `geo-lsep`  0  THEN  Auto))
  THEN  (Assert  p  leftof  xy  BY
                          (InstLemma  `left-convex2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto))
  )

---

Home Index