---

Step * of Lemma symmetry-preserves-right-angle

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  Auto  THEN  RenameVar  `x'  (-2))

---

Home Index