---

Step * of Lemma geo-left-out-better

No Annotations
∀e:EuclideanPlane. ∀a,b,a',p:Point.  (p leftof ba ⇒ b # a' ⇒ (¬((¬B(baa')) ∧ (¬B(ba'a)))) ⇒ p leftof ba')
BY
{ (Auto
   THEN (Assert p # ba BY
               (OrLeft THEN Auto))
   THEN (Assert Colinear(b;a;a') BY
               (((D 0 THENA Auto) THEN D -3 THEN Auto)
                THEN Try (((D 0 THEN Auto)
                           THEN (Assert Colinear(b;a;a') BY
                                       Auto)
                           THEN Unfold `geo-colinear` -1
                           THEN Auto))
                ))
   THEN (Assert p # ba' BY
               Auto)
   THEN D -1
   THEN Try (Trivial)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a' : Point
5. p : Point
6. p leftof ba
7. b # a'
8. ¬((¬B(baa')) ∧ (¬B(ba'a)))
9. p # ba
10. Colinear(b;a;a')
11. p leftof a'b
⊢ p leftof ba'

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,a',p:Point.
    (p  leftof  ba  {}\mRightarrow{}  b  \#  a'  {}\mRightarrow{}  (\mneg{}((\mneg{}B(baa'))  \mwedge{}  (\mneg{}B(ba'a))))  {}\mRightarrow{}  p  leftof  ba')


By

---

Latex:
(Auto
  THEN  (Assert  p  \#  ba  BY
                          (OrLeft  THEN  Auto))
  THEN  (Assert  Colinear(b;a;a')  BY
                          (((D  0  THENA  Auto)  THEN  D  -3  THEN  Auto)
                            THEN  Try  (((D  0  THEN  Auto)
                                                  THEN  (Assert  Colinear(b;a;a')  BY
                                                                          Auto)
                                                  THEN  Unfold  `geo-colinear`  -1
                                                  THEN  Auto))
                            ))
  THEN  (Assert  p  \#  ba'  BY
                          Auto)
  THEN  D  -1
  THEN  Try  (Trivial))

---

Home Index