---

Step * 2 2 of Lemma lt-angle-not-cong


1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. ¬x # yz
6. Colinear(x;y;z)
7. xyz < xyz
8. y ≡ z
⊢ False
BY
{ ((Assert y ≠ z BY ((D -2 THEN ExRepD) THEN EAuto 1)) THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  x  :  Point
3.  y  :  Point
4.  z  :  Point
5.  \mneg{}x  \#  yz
6.  Colinear(x;y;z)
7.  xyz  <  xyz
8.  y  \mequiv{}  z
\mvdash{}  False


By

---

Latex:
((Assert  y  \mneq{}  z  BY  ((D  -2  THEN  ExRepD)  THEN  EAuto  1))  THEN  Auto)

---

Home Index