---

Step * of Lemma geo-out_transitivity

∀e:BasicGeometry. ∀a,b,c,d:Point.  (out(a bc) ⇒ out(a cd) ⇒ out(a bd))
BY
{ (Auto
   THEN All (Unfold  `geo-out`)
   THEN ExRepD
   THEN RepeatFor 3 (((D 0 THENA Auto) THEN Try (Trivial)))
   THEN (DNot 11 THEN ((D 0 THEN D 0) THENA Auto))
   THEN DNot 8
   THEN ((D 0 THEN D 0) THENA Auto)
   THEN ExRepD) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. a ≠ c
8. a ≠ c
9. a ≠ d
10. ¬a_b_d
11. ¬a_d_b
12. a_c_d
13. a_b_c
⊢ False

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. a ≠ c
8. a ≠ c
9. a ≠ d
10. ¬a_b_d
11. ¬a_d_b
12. a_c_d
13. a_c_b
⊢ False

3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. a ≠ c
8. a ≠ c
9. a ≠ d
10. ¬a_b_d
11. ¬a_d_b
12. a_d_c
13. a_b_c
⊢ False

4
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. a ≠ c
8. a ≠ c
9. a ≠ d
10. ¬a_b_d
11. ¬a_d_b
12. a_d_c
13. a_c_b
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (out(a  bc)  {}\mRightarrow{}  out(a  cd)  {}\mRightarrow{}  out(a  bd))


By

---

Latex:
(Auto
  THEN  All  (Unfold    `geo-out`)
  THEN  ExRepD
  THEN  RepeatFor  3  (((D  0  THENA  Auto)  THEN  Try  (Trivial)))
  THEN  (DNot  11  THEN  ((D  0  THEN  D  0)  THENA  Auto))
  THEN  DNot  8
  THEN  ((D  0  THEN  D  0)  THENA  Auto)
  THEN  ExRepD)

---

Home Index