---

Step * of Lemma test-prove-distinct

∀e:EuclideanPlane. ∀A,B,C,X,Y,Z,W,U,V:Point.
  ((Colinear(A;B;X) ∨ A-X-B ∨ B-X-A)
  ⇒ (A_B_C ∨ C_B_A)
  ⇒ (Y_C_A ∨ A_C_Y)
  ⇒ (ZW=AY ∨ ZW=YA)
  ⇒ ZW=UV
  ⇒ (¬(U = V ∈ Point)))
BY
{ Auto }

1
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)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C,X,Y,Z,W,U,V:Point.
    ((Colinear(A;B;X)  \mvee{}  A-X-B  \mvee{}  B-X-A)
    {}\mRightarrow{}  (A\_B\_C  \mvee{}  C\_B\_A)
    {}\mRightarrow{}  (Y\_C\_A  \mvee{}  A\_C\_Y)
    {}\mRightarrow{}  (ZW=AY  \mvee{}  ZW=YA)
    {}\mRightarrow{}  ZW=UV
    {}\mRightarrow{}  (\mneg{}(U  =  V)))


By

---

Latex:
Auto

---

Home Index