---

Step * of Lemma geo-out-strict_transitivity

∀e:BasicGeometry. ∀a,b,c,d:Point.
  (b ≠ d ⇒ geo-out-strict(e;a;b;c) ⇒ geo-out-strict(e;a;c;d) ⇒ geo-out-strict(e;a;b;d))
BY
{ (((((Auto THEN All (Unfold  `geo-out-strict`)) THEN D 0) THENA Auto) THEN D -1)
   THEN (DNot 8 THEN (RepeatFor 2 (D 0) THENA Auto))
   THEN (DNot 7 THEN (RepeatFor 2 (D 0) THENA Auto))
   THEN Try (Complete (Auto))) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b ≠ d
7. ¬a-b-d
8. ¬a-d-b
9. a-c-d
10. a-c-b
⊢ False

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b ≠ d
7. ¬a-b-d
8. ¬a-d-b
9. a-d-c
10. a-b-c
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.
    (b  \mneq{}  d  {}\mRightarrow{}  geo-out-strict(e;a;b;c)  {}\mRightarrow{}  geo-out-strict(e;a;c;d)  {}\mRightarrow{}  geo-out-strict(e;a;b;d))


By

---

Latex:
(((((Auto  THEN  All  (Unfold    `geo-out-strict`))  THEN  D  0)  THENA  Auto)  THEN  D  -1)
  THEN  (DNot  8  THEN  (RepeatFor  2  (D  0)  THENA  Auto))
  THEN  (DNot  7  THEN  (RepeatFor  2  (D  0)  THENA  Auto))
  THEN  Try  (Complete  (Auto)))

---

Home Index