---

Step * of Lemma right-angle-colinear2

∀e:BasicGeometry. ∀a,b,c,c':Point.  (Rabc ⇒ c ≠ b ⇒ Colinear(b;c;c') ⇒ Rabc')
BY
{ (Auto THEN (gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THENA Auto)) }

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

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. c' : Point
6. Rbbc
7. c ≠ b
8. Colinear(b;c;c')
9. a ≡ b
⊢ Rbbc'

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index