---

Step * of Lemma geo-vert-angle-SAS

∀e:BasicGeometry. ∀a,p,q,p',q':Point.  (p-a-q ⇒ p'-a-q' ⇒ pa ≅ p'a ⇒ qa ≅ q'a ⇒ p'q ≅ pq')
BY
{ ((Auto THEN gSeparatedCases ⌜p⌝⌜p'⌝⋅) THEN Auto) }

1
1. e : BasicGeometry
2. a : Point
3. p : Point
4. q : Point
5. p' : Point
6. q' : Point
7. p-a-q
8. p'-a-q'
9. pa ≅ p'a
10. qa ≅ q'a
11. p ≠ p'
⊢ p'q ≅ pq'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,p,q,p',q':Point.    (p-a-q  {}\mRightarrow{}  p'-a-q'  {}\mRightarrow{}  pa  \mcong{}  p'a  {}\mRightarrow{}  qa  \mcong{}  q'a  {}\mRightarrow{}  p'q  \mcong{}  pq')


By

---

Latex:
((Auto  THEN  gSeparatedCases  \mkleeneopen{}p\mkleeneclose{}\mkleeneopen{}p'\mkleeneclose{}\mcdot{})  THEN  Auto)

---

Home Index