---

Step * 1 1 2 2 2 2 of Lemma eu-cong-angle-symm


1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. ¬(a = b ∈ Point)
6. ¬(c = b ∈ Point)
⊢ ∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ b_c_x' ∧ b_a_z' ∧ ba'=bx' ∧ bc'=bz' ∧ a'c'=x'z')
BY
{ ((Prolong ⌜b⌝ ⌜a⌝ `x' ⌜b⌝ ⌜c⌝⋅ THENA Auto)
   THEN (Prolong ⌜b⌝ ⌜c⌝ `y' ⌜b⌝ ⌜a⌝⋅ THENA Auto)
   THEN InstConcl [⌜x⌝;⌜y⌝;⌜y⌝;⌜x⌝]⋅
   THEN Auto) }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. ¬(a = b ∈ Point)
6. ¬(c = b ∈ Point)
7. x : Point
8. b_a_x
9. ax=bc
10. y : Point
11. b_c_y
12. cy=ba
13. b_a_x
14. b_c_y
15. b_c_y
16. b_a_x
⊢ bx=by

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  a  :  Point@i
3.  b  :  Point@i
4.  c  :  Point@i
5.  \mneg{}(a  =  b)
6.  \mneg{}(c  =  b)
\mvdash{}  \mexists{}a',c',x',z':Point.  (b\_a\_a'  \mwedge{}  b\_c\_c'  \mwedge{}  b\_c\_x'  \mwedge{}  b\_a\_z'  \mwedge{}  ba'=bx'  \mwedge{}  bc'=bz'  \mwedge{}  a'c'=x'z')


By

---

Latex:
((Prolong  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}  `x'  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Prolong  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  `y'  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index