---

Step * 1 of Lemma p5eu


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ab=ac
6. Triangle(a;b;c)
⊢ ∃j,k:Point. jbc = kcb
BY
{ Unfold `eu-tri` 6 }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ab=ac
6. (¬(a = b ∈ Point)) ∧ (¬(a = c ∈ Point)) ∧ (¬(b = c ∈ Point))
⊢ ∃j,k:Point. jbc = kcb

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  ab=ac
6.  Triangle(a;b;c)
\mvdash{}  \mexists{}j,k:Point.  jbc  =  kcb


By

---

Latex:
Unfold  `eu-tri`  6

---

Home Index