---

Step * of Lemma interior-angles-unique

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d,b',c',p:Point.
  (a # bc ⇒ out(b dc) ⇒ out(a bb') ⇒ out(a cc') ⇒ B(b'pc') ⇒ p # c' ⇒ bad < bac ⇒ bap ≅a bad ⇒ out(a dp))
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. a # bc
10. out(b dc)
11. out(a bb')
12. out(a cc')
13. B(b'pc')
14. p # c'
15. bad < bac
16. bap ≅a bad
⊢ out(a dp)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d,b',c',p:Point.
    (a  \#  bc
    {}\mRightarrow{}  out(b  dc)
    {}\mRightarrow{}  out(a  bb')
    {}\mRightarrow{}  out(a  cc')
    {}\mRightarrow{}  B(b'pc')
    {}\mRightarrow{}  p  \#  c'
    {}\mRightarrow{}  bad  <  bac
    {}\mRightarrow{}  bap  \mcong{}\msuba{}  bad
    {}\mRightarrow{}  out(a  dp))


By

---

Latex:
Auto

---

Home Index