---

Step * 1 of Lemma geo-bet-out-out-bet


1. e : BasicGeometry
2. b : Point
3. a : Point
4. a' : Point
5. c : Point
6. c' : Point
7. a_b_c
8. b ≠ a
9. b ≠ a'
10. ¬((¬b_a_a') ∧ (¬b_a'_a))
11. b ≠ c
12. b ≠ c'
13. ¬((¬b_c_c') ∧ (¬b_c'_c))
14. ¬a'_b_c'
⊢ False
BY
{ ((D 10 THEN (RepeatFor 2 (D 0) THENA Auto)) THEN D 12 THEN (RepeatFor 2 (D 0) THENA Auto) THEN D 12 THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  b  :  Point
3.  a  :  Point
4.  a'  :  Point
5.  c  :  Point
6.  c'  :  Point
7.  a\_b\_c
8.  b  \mneq{}  a
9.  b  \mneq{}  a'
10.  \mneg{}((\mneg{}b\_a\_a')  \mwedge{}  (\mneg{}b\_a'\_a))
11.  b  \mneq{}  c
12.  b  \mneq{}  c'
13.  \mneg{}((\mneg{}b\_c\_c')  \mwedge{}  (\mneg{}b\_c'\_c))
14.  \mneg{}a'\_b\_c'
\mvdash{}  False


By

---

Latex:
((D  10  THEN  (RepeatFor  2  (D  0)  THENA  Auto))
  THEN  D  12
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  D  12
  THEN  Auto)

---

Home Index