---

Step * of Lemma geo-left-out-2

∀e:EuclideanPlane. ∀a,b,p,p':Point.  (p leftof ba ⇒ out(b pp') ⇒ p' leftof ba)
BY
{ (Auto
   THEN (Assert p # ba BY
               (OrLeft THEN Auto))
   THEN (Assert p' # ba BY
               Auto)
   THEN D -1
   THEN Auto
   THEN Assert ⌜False⌝⋅
   THEN Auto) }

1
.....assertion..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. p : Point
5. p' : Point
6. p leftof ba
7. out(b pp')
8. p # ba
9. p' leftof ab
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,p,p':Point.    (p  leftof  ba  {}\mRightarrow{}  out(b  pp')  {}\mRightarrow{}  p'  leftof  ba)


By

---

Latex:
(Auto
  THEN  (Assert  p  \#  ba  BY
                          (OrLeft  THEN  Auto))
  THEN  (Assert  p'  \#  ba  BY
                          Auto)
  THEN  D  -1
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index