---

Step * of Lemma right-angle-legs-same

∀e:BasicGeometry. ∀a,b:Point.  (Rbab ⇒ a ≡ b)
BY
{ (Auto THEN gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THEN Auto THEN Unfold `right-angle` -2) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. ∀c':Point. (c'=a=b ⇒ bb ≅ bc')
5. a ≠ b
⊢ a ≡ b

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b:Point.    (Rbab  {}\mRightarrow{}  a  \mequiv{}  b)


By

---

Latex:
(Auto  THEN  gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Unfold  `right-angle`  -2)

---

Home Index