---

Step * 1 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'
12. q ≠ q'
⊢ p'q ≅ pq'
BY
{ (((((PropergProlong ⌜a⌝⌜q⌝ `r1' ⌜a⌝⌜p⌝⋅ THENA Auto) THEN (PropergProlong ⌜a⌝⌜q'⌝ `r2' ⌜a⌝⌜p⌝⋅ THENA Auto))
     THEN (PropergProlong ⌜a⌝⌜p⌝ `r3' ⌜a⌝⌜q⌝⋅ THENA Auto)
     )
    THEN (PropergProlong ⌜a⌝⌜p'⌝ `r4' ⌜a⌝⌜q⌝⋅ THENA Auto)
    )
   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'
12. q ≠ q'
13. r1 : Point
14. a-q-r1
15. qr1 ≅ ap
16. r2 : Point
17. a-q'-r2
18. q'r2 ≅ ap
19. r3 : Point
20. a-p-r3
21. pr3 ≅ aq
22. r4 : Point
23. a-p'-r4
24. p'r4 ≅ aq
⊢ 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'
12.  q  \mneq{}  q'
\mvdash{}  p'q  \mcong{}  pq'


By

---

Latex:
(((((PropergProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}q\mkleeneclose{}  `r1'  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}p\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  (PropergProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}q'\mkleeneclose{}  `r2'  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}p\mkleeneclose{}\mcdot{}  THENA  Auto)
        )
      THEN  (PropergProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}p\mkleeneclose{}  `r3'  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  Auto)
      )
    THEN  (PropergProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}p'\mkleeneclose{}  `r4'  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  Auto)
    )
  THEN  Auto
  )

---

Home Index