---

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

No Annotations
∀e:EuclideanPlane. ∀a,b,c,q:Point.  (a leftof bc ⇒ q leftof bc ⇒ qbc ≅a abc ⇒ out(b aq))
BY
{ (Auto
   THEN ((gProperProlong ⌜a⌝ ⌜b⌝ `u' ⌜O⌝ ⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜u⌝ ⌜b⌝ `q1' ⌜b⌝ ⌜q⌝⋅ THENA (Auto THEN D -4 THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. q : Point
6. a leftof bc
7. q leftof bc
8. qbc ≅a abc
9. u : Point
10. a-b-u
11. bu ≅ OX
12. q1 : Point
13. u-b-q1 ∧ bq1 ≅ bq
⊢ out(b aq)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,q:Point.    (a  leftof  bc  {}\mRightarrow{}  q  leftof  bc  {}\mRightarrow{}  qbc  \mcong{}\msuba{}  abc  {}\mRightarrow{}  out(b  aq))


By

---

Latex:
(Auto
  THEN  ((gProperProlong  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  `u'  \mkleeneopen{}O\mkleeneclose{}  \mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}u\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  `q1'  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  D  -4  THEN  Auto)))

---

Home Index