---

Step * 1 of Lemma geo-inner-three-segment


1. e : EuclideanPlane
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. ∀[d,A,B,C,D:Point].  (bd ≅ BD) supposing (cd ≅ CD and ad ≅ AD and bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
⊢ ∀[A,B,C:Point].  (ab ≅ AB) supposing (bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
BY
{ ((InstHyp [⌜a⌝] (-1)⋅ THENA Auto) THEN RepeatFor 3 (ParallelLast') THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ∀[d,A,B,C,D:Point].  (bd ≅ BD) supposing (cd ≅ CD and ad ≅ AD and bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
6. A : Point
7. B : Point
8. C : Point
9. ∀[D:Point]. (ba ≅ BD) supposing (ca ≅ CD and aa ≅ AD and bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
10. B(abc)
11. B(ABC)
12. ac ≅ AC
13. bc ≅ BC
⊢ ab ≅ AB

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  [a]  :  Point
3.  [b]  :  Point
4.  [c]  :  Point
5.  \mforall{}[d,A,B,C,D:Point].
          (bd  \mcong{}  BD)  supposing  (cd  \mcong{}  CD  and  ad  \mcong{}  AD  and  bc  \mcong{}  BC  and  ac  \mcong{}  AC  and  B(ABC)  and  B(abc))
\mvdash{}  \mforall{}[A,B,C:Point].    (ab  \mcong{}  AB)  supposing  (bc  \mcong{}  BC  and  ac  \mcong{}  AC  and  B(ABC)  and  B(abc))


By

---

Latex:
((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  RepeatFor  3  (ParallelLast')  THEN  Auto)

---

Home Index