---

Step * of Lemma Euclid-Prop5

∀e:EuclideanPlane. ∀a,b,c,x,y:Point.  (((ab ≅ ac ∧ a # bc) ∧ a-b-x ∧ a-c-y) ⇒ (abc ≅a acb ∧ xbc ≅a ycb))
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. ab ≅ ac
8. a # bc
9. a-b-x
10. a-c-y
⊢ abc ≅a acb

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. ab ≅ ac
8. a # bc
9. a-b-x
10. a-c-y
11. abc ≅a acb
⊢ xbc ≅a ycb

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y:Point.
    (((ab  \00D0  ac  \mwedge{}  a  \#  bc)  \mwedge{}  a-b-x  \mwedge{}  a-c-y)  {}\mRightarrow{}  (abc  \00D0\msuba{}  acb  \mwedge{}  xbc  \00D0\msuba{}  ycb))


By

---

Latex:
Auto

---

Home Index