---

Step * of Lemma test-prove-separated

∀e:BasicGeometry. ∀A,B,C,X,Y,Z,W,U,V:Point.
  ((A ≠ B ∨ 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)
BY
{ (Auto THEN SplitOrHyps THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,C,X,Y,Z,W,U,V:Point.
    ((A  \mneq{}  B  \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  \00D0  AY  \mvee{}  ZW  \00D0  YA)
    {}\mRightarrow{}  ZW  \00D0  UV
    {}\mRightarrow{}  U  \mneq{}  V)


By

---

Latex:
(Auto  THEN  SplitOrHyps  THEN  Auto)

---

Home Index