---

Step * 1 2 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. q'a ≅ q'a
11. p ≠ p'
12. q ≡ q'
⊢ p'q' ≅ pq'
BY
{ Assert ⌜False⌝⋅ }

1
.....assertion..... 
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'
⊢ False

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'
13. False
⊢ 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.  q'a  \mcong{}  q'a
11.  p  \mneq{}  p'
12.  q  \mequiv{}  q'
\mvdash{}  p'q'  \mcong{}  pq'


By

---

Latex:
Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}

---

Home Index