---

Step * of Lemma right-angles-not-acute2

∀e:BasicGeometry. ∀a,b,c,a':Point.  (b ≠ c ⇒ Rabc ⇒ Ra'bc ⇒ a_a'_c ⇒ a ≡ a')
BY
{ (Auto
   THEN gSeparatedCases ⌜b⌝ ⌜c⌝⋅
   THEN Auto
   THEN gSeparatedCases ⌜a'⌝ ⌜a⌝⋅
   THEN Auto
   THEN gEliminatePoints
   THEN Auto) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b ≠ c
7. Rabc
8. Ra'bc
9. a_a'_c
10. b ≠ c
11. a' ≠ a
⊢ a ≡ a'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a':Point.    (b  \mneq{}  c  {}\mRightarrow{}  Rabc  {}\mRightarrow{}  Ra'bc  {}\mRightarrow{}  a\_a'\_c  {}\mRightarrow{}  a  \mequiv{}  a')


By

---

Latex:
(Auto
  THEN  gSeparatedCases  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  gSeparatedCases  \mkleeneopen{}a'\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  gEliminatePoints
  THEN  Auto)

---

Home Index