---

Step * 1 of Lemma test-prove-distinct


1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. X : Point
6. Y : Point
7. Z : Point
8. W : Point
9. U : Point
10. V : Point
11. Colinear(A;B;X) ∨ A-X-B ∨ B-X-A
12. A_B_C ∨ C_B_A
13. Y_C_A ∨ A_C_Y
14. ZW=AY ∨ ZW=YA
15. ZW=UV
⊢ ¬(U = V ∈ Point)
BY
{ (SplitOrHyps THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  X  :  Point
6.  Y  :  Point
7.  Z  :  Point
8.  W  :  Point
9.  U  :  Point
10.  V  :  Point
11.  Colinear(A;B;X)  \mvee{}  A-X-B  \mvee{}  B-X-A
12.  A\_B\_C  \mvee{}  C\_B\_A
13.  Y\_C\_A  \mvee{}  A\_C\_Y
14.  ZW=AY  \mvee{}  ZW=YA
15.  ZW=UV
\mvdash{}  \mneg{}(U  =  V)


By

---

Latex:
(SplitOrHyps  THEN  Auto)

---

Home Index