---

Step * of Lemma colinear-right-angle

∀e:BasicGeometry. ∀a,b,c:Point.  (b ≠ c ⇒ Colinear(a;b;c) ⇒ Rabc ⇒ a ≡ b)
BY
{ (Auto THEN gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THEN Auto THEN Assert ⌜Raba⌝⋅ THEN EAuto 2) }

1
.....assertion..... 
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. b ≠ c
6. Colinear(a;b;c)
7. Rabc
8. a ≠ b
⊢ Raba

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (b  \mneq{}  c  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  Rabc  {}\mRightarrow{}  a  \mequiv{}  b)


By

---

Latex:
(Auto  THEN  gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Assert  \mkleeneopen{}Raba\mkleeneclose{}\mcdot{}  THEN  EAuto  2)

---

Home Index