---

Step * of Lemma p5-triangles

No Annotations
∀e:HeytingGeometry. ∀a,b,c:Point.  (a # bc ⇒ ab ≅ cb ⇒ (bac ≅a bca ∧ (∀p,q:Point.  ((b-a-p ∧ b-c-q) ⇒ pac ≅a qca))))
BY
{ (Auto THEN Unfold `geo-cong-angle` 0) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. ab ≅ cb
⊢ (((b # a ∧ a # c) ∧ b # c) ∧ c # a)
∧ (∃a',c',x',z':Point. (B(aba') ∧ B(acc') ∧ B(cbx') ∧ B(caz') ∧ aa' ≅ cx' ∧ ac' ≅ cz' ∧ a'c' ≅ x'z'))

2
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
⊢ (((p # a ∧ a # c) ∧ q # c) ∧ c # a)
∧ (∃a',c',x',z':Point. (B(apa') ∧ B(acc') ∧ B(cqx') ∧ B(caz') ∧ aa' ≅ cx' ∧ ac' ≅ cz' ∧ a'c' ≅ x'z'))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.
    (a  \#  bc  {}\mRightarrow{}  ab  \mcong{}  cb  {}\mRightarrow{}  (bac  \mcong{}\msuba{}  bca  \mwedge{}  (\mforall{}p,q:Point.    ((b-a-p  \mwedge{}  b-c-q)  {}\mRightarrow{}  pac  \mcong{}\msuba{}  qca))))


By

---

Latex:
(Auto  THEN  Unfold  `geo-cong-angle`  0)

---

Home Index