---

Step * 2 1 of Lemma p5-triangles


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
7. bac ≅a bca
8. p : Point
9. q : Point
10. b-a-p
11. b-c-q
⊢ ∃a',c',x',z':Point. (B(apa') ∧ B(acc') ∧ B(cqx') ∧ B(caz') ∧ aa' ≅ cx' ∧ ac' ≅ cz' ∧ a'c' ≅ x'z')
BY
{ ((((PropergProlong ⌜a⌝⌜p⌝`a\''⌜c⌝⌜q⌝⋅ THENA Auto) THEN (PropergProlong ⌜c⌝⌜q⌝`x\''⌜a⌝⌜p⌝⋅ THENA Auto))
    THEN (ExRepD THEN InstConcl [⌜a'⌝;⌜c⌝;⌜x'⌝;⌜a⌝]⋅)
    THEN Auto)
   THEN InstLemma `geo-five-segment` [⌜e⌝;⌜b⌝;⌜a⌝;⌜a'⌝;⌜c⌝;⌜b⌝;⌜c⌝;⌜x'⌝;⌜a⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  ab  \mcong{}  cb
7.  bac  \mcong{}\msuba{}  bca
8.  p  :  Point
9.  q  :  Point
10.  b-a-p
11.  b-c-q
\mvdash{}  \mexists{}a',c',x',z':Point.  (B(apa')  \mwedge{}  B(acc')  \mwedge{}  B(cqx')  \mwedge{}  B(caz')  \mwedge{}  aa'  \mcong{}  cx'  \mwedge{}  ac'  \mcong{}  cz'  \mwedge{}  a'c'  \mcong{}  x'z')


By

---

Latex:
((((PropergProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}p\mkleeneclose{}`a\mbackslash{}''\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  Auto)
      THEN  (PropergProlong  \mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}q\mkleeneclose{}`x\mbackslash{}''\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}p\mkleeneclose{}\mcdot{}  THENA  Auto)
      )
    THEN  (ExRepD  THEN  InstConcl  [\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{})
    THEN  Auto)
  THEN  InstLemma  `geo-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index