---

Step * 1 of Lemma geo-between-middle-or


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. b ≠ c
8. b ≠ d
9. a_b_d
10. a_c_d
11. c1 : Point
12. a-b-c1
13. bc1 ≅ bc
14. c2 : Point
15. c1-b-c2
16. bc2 ≅ bc
17. ¬¬(b_c_d ∨ c_b_d)
18. c1 ≠ c
⊢ b_c_d ∨ c_b_d
BY
{ ((OrRight THEN Auto)
   THEN ((((DoubleNegation THENM SupposeMore (-2)) THENA Auto) THEN (RemoveDoubleNegation THENA Auto))
         THEN D -1
         THEN Auto)
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN InstLemma `geo-construction-unicity` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜c1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \mneq{}  b
7.  b  \mneq{}  c
8.  b  \mneq{}  d
9.  a\_b\_d
10.  a\_c\_d
11.  c1  :  Point
12.  a-b-c1
13.  bc1  \mcong{}  bc
14.  c2  :  Point
15.  c1-b-c2
16.  bc2  \mcong{}  bc
17.  \mneg{}\mneg{}(b\_c\_d  \mvee{}  c\_b\_d)
18.  c1  \mneq{}  c
\mvdash{}  b\_c\_d  \mvee{}  c\_b\_d


By

---

Latex:
((OrRight  THEN  Auto)
  THEN  ((((DoubleNegation  THENM  SupposeMore  (-2))  THENA  Auto)  THEN  (RemoveDoubleNegation  THENA  Auto))
              THEN  D  -1
              THEN  Auto)
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  InstLemma  `geo-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index