---

Step * of Lemma right-angle-symmetry

∀e:BasicGeometry. ∀a,b,c:Point.  (Rabc ⇒ Rcba)
BY
{ (Auto THEN ParallelLast THEN Auto THEN RenameVar `a\'' (-2)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
6. a' : Point
7. a'=b=a
⊢ ca ≅ ca'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (Rabc  {}\mRightarrow{}  Rcba)


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  Auto  THEN  RenameVar  `a\mbackslash{}''  (-2))

---

Home Index