---

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

.....antecedent..... 
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. c2 ≠ c
18. c_b_d
⊢ d_b_c2
BY
{ ((InstLemma `extended-out-preserves-between` [⌜e⌝;⌜b⌝;⌜c1⌝;⌜d⌝;⌜c2⌝]⋅ THEN Auto)
   THEN InstLemma `geo-out-iff-between1` [⌜e⌝;⌜b⌝;⌜c1⌝;⌜d⌝;⌜a⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
.....antecedent..... 
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.  c2  \mneq{}  c
18.  c\_b\_d
\mvdash{}  d\_b\_c2


By

---

Latex:
((InstLemma  `extended-out-preserves-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index