---

Step * 1 of Lemma geo-between-outer-trans


1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b # c
7. B(abc)
8. B(bcd)
9. a # c
⊢ B(acd)
BY
{ ((gProlong ⌜a⌝ ⌜c⌝ `x' ⌜c⌝ ⌜d⌝⋅ THENA Auto)
   THEN InstLemma `geo-construction-unicity` [⌜e⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜d⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry-
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  b  \#  c
7.  B(abc)
8.  B(bcd)
9.  a  \#  c
\mvdash{}  B(acd)


By

---

Latex:
((gProlong  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  `x'  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  InstLemma  `geo-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index