---

Step * of Lemma geo-between-middle-or

∀e:BasicGeometry. ∀a,b,c,d:Point.  (a ≠ b ⇒ b ≠ c ⇒ b ≠ d ⇒ a_b_d ⇒ a_c_d ⇒ (b_c_d ∨ c_b_d))
BY
{ (Auto
   THEN ((gProperProlong ⌜a⌝⌜b⌝`c1'⌜b⌝⌜c⌝⋅ THENA Auto) THEN ExRepD)
   THEN ((gProperProlong ⌜c1⌝⌜b⌝`c2'⌜b⌝⌜c⌝⋅ THENA Auto) THEN ExRepD)
   THEN (Assert ¬¬(b_c_d ∨ c_b_d) BY
               ((Assert (¬((¬b_c_d) ∧ (¬c_b_d))) ⇒ (¬¬(b_c_d ∨ c_b_d)) BY
                       Auto)
                THEN InstLemma `geo-between-middle` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅
                THEN Auto))
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜c1⌝;⌜c2⌝;⌜c⌝]⋅ THENA Auto)
   THEN D -1) }

1
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

2
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. c2 ≠ c
⊢ b_c_d ∨ c_b_d

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (a  \mneq{}  b  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  b  \mneq{}  d  {}\mRightarrow{}  a\_b\_d  {}\mRightarrow{}  a\_c\_d  {}\mRightarrow{}  (b\_c\_d  \mvee{}  c\_b\_d))


By

---

Latex:
(Auto
  THEN  ((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`c1'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  ((gProperProlong  \mkleeneopen{}c1\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`c2'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (Assert  \mneg{}\mneg{}(b\_c\_d  \mvee{}  c\_b\_d)  BY
                          ((Assert  (\mneg{}((\mneg{}b\_c\_d)  \mwedge{}  (\mneg{}c\_b\_d)))  {}\mRightarrow{}  (\mneg{}\mneg{}(b\_c\_d  \mvee{}  c\_b\_d))  BY
                                          Auto)
                            THEN  InstLemma  `geo-between-middle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index