---

Step * 2 of Lemma out-implies-straightangle


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a' ≠ b'
9. c' ≠ b'
10. out(b ac)
11. out(b' a'c')
⊢ abc ≅a a'b'c'
BY
{ ((gSymmetricPoint ⌜b'⌝⌜a'⌝`A\''⋅ THENA Auto)
   THEN (gProperProlong  ⌜A'⌝⌜b'⌝`p'⌜b⌝⌜a⌝⋅ THENA Auto)
   THEN (gProperProlong  ⌜A'⌝⌜b'⌝`q'⌜b⌝⌜c⌝⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a' ≠ b'
9. c' ≠ b'
10. out(b ac)
11. out(b' a'c')
12. A' : Point
13. a'=b'=A'
14. p : Point
15. A'-b'-p ∧ b'p ≅ ba
16. q : Point
17. A'-b'-q ∧ b'q ≅ bc
⊢ abc ≅a a'b'c'

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  b'  :  Point
7.  c'  :  Point
8.  a'  \mneq{}  b'
9.  c'  \mneq{}  b'
10.  out(b  ac)
11.  out(b'  a'c')
\mvdash{}  abc  \mcong{}\msuba{}  a'b'c'


By

---

Latex:
((gSymmetricPoint  \mkleeneopen{}b'\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}`A\mbackslash{}''\mcdot{}  THENA  Auto)
  THEN  (gProperProlong    \mkleeneopen{}A'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`p'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong    \mkleeneopen{}A'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`q'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index