---

Step * 1 of Lemma geo-vert-angle-SAS


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'
BY
{ (gSeparatedCases ⌜q⌝⌜q'⌝⋅ THENA 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'
12. q ≠ q'
⊢ p'q ≅ pq'

2
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. q'a ≅ q'a
11. p ≠ p'
12. q ≡ q'
⊢ p'q' ≅ pq'

---

Latex:

---

Latex:

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  \mcong{}  p'a
10.  qa  \mcong{}  q'a
11.  p  \mneq{}  p'
\mvdash{}  p'q  \mcong{}  pq'


By

---

Latex:
(gSeparatedCases  \mkleeneopen{}q\mkleeneclose{}\mkleeneopen{}q'\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index