---

Step * 1 of Lemma colinear-right-angle

.....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
BY
{ (Using [`c',⌜c⌝] (BLemma `right-angle-colinear2`)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  b  \mneq{}  c
6.  Colinear(a;b;c)
7.  Rabc
8.  a  \mneq{}  b
\mvdash{}  Raba


By

---

Latex:
(Using  [`c',\mkleeneopen{}c\mkleeneclose{}]  (BLemma  `right-angle-colinear2`)\mcdot{}  THEN  Auto)

---

Home Index