---

Step * of Lemma geo-lt-angle-triangle-point-exists

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (abc < xyz ⇒ a # bc ⇒ x # yz ⇒ (∃p:Point. (x-p-z ∧ xyp ≅a abc)))
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. a # bc
10. x # yz
⊢ ∃p:Point. (x-p-z ∧ xyp ≅a abc)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    (abc  <  xyz  {}\mRightarrow{}  a  \#  bc  {}\mRightarrow{}  x  \#  yz  {}\mRightarrow{}  (\mexists{}p:Point.  (x-p-z  \mwedge{}  xyp  \mcong{}\msuba{}  abc)))


By

---

Latex:
Auto

---

Home Index