---

Step * 1 of Lemma unique-angles-in-half-plane


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
⊢ ∃f:Point. (acb ≅a fzy ∧ (x leftof yz ⇐⇒ f leftof yz) ∧ (x leftof zy ⇐⇒ f leftof zy))
BY
{ ((gProlong ⌜c⌝ ⌜b⌝ `u' ⌜z⌝ ⌜y⌝⋅ THENA Auto) THEN (gProlong ⌜z⌝ ⌜y⌝ `v' ⌜c⌝ ⌜b⌝⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. u : Point
11. B(cbu) ∧ bu ≅ zy
12. v : Point
13. B(zyv) ∧ yv ≅ cb
⊢ ∃f:Point. (acb ≅a fzy ∧ (x leftof yz ⇐⇒ f leftof yz) ∧ (x leftof zy ⇐⇒ f leftof zy))

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a  \#  bc
9.  x  \#  yz
\mvdash{}  \mexists{}f:Point.  (acb  \mcong{}\msuba{}  fzy  \mwedge{}  (x  leftof  yz  \mLeftarrow{}{}\mRightarrow{}  f  leftof  yz)  \mwedge{}  (x  leftof  zy  \mLeftarrow{}{}\mRightarrow{}  f  leftof  zy))


By

---

Latex:
((gProlong  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  `u'  \mkleeneopen{}z\mkleeneclose{}  \mkleeneopen{}y\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (gProlong  \mkleeneopen{}z\mkleeneclose{}  \mkleeneopen{}y\mkleeneclose{}  `v'  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index