---

Step * 2 of Lemma geo-colinear-five-segment


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. a # b
11. Colinear(a;b;c)
12. ac ≅ AC
13. ab ≅ AB
14. bc ≅ BC
15. ad ≅ AD
16. bd ≅ BD
17. B(bca)
⊢ cd ≅ CD
BY
{ ((InstLemma `geo-congruent-preserves-between` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜A⌝;⌜C⌝;⌜B⌝]⋅ THENA Auto)
   THEN InstLemma `geo-inner-five-segment` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜d⌝;⌜A⌝;⌜C⌝;⌜B⌝;⌜D⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  A  :  Point
7.  B  :  Point
8.  C  :  Point
9.  D  :  Point
10.  a  \#  b
11.  Colinear(a;b;c)
12.  ac  \mcong{}  AC
13.  ab  \mcong{}  AB
14.  bc  \mcong{}  BC
15.  ad  \mcong{}  AD
16.  bd  \mcong{}  BD
17.  B(bca)
\mvdash{}  cd  \mcong{}  CD


By

---

Latex:
((InstLemma  `geo-congruent-preserves-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `geo-inner-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index