---

Step * of Lemma right-angles-not-acute

∀e:BasicGeometry. ∀a,b,c,a':Point.  (Rabc ⇒ Ra'bc ⇒ a_c_a' ⇒ b ≡ c)
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. Rabc
7. Ra'bc
8. a_c_a'
9. b ≠ c
10. a' ≠ a
⊢ b ≡ c

---

Latex:

---

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


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