---

Step * of Lemma geo-lt-angle-degenerate-case2

No Annotations
∀e:EuclideanPlane. ∀a,b,x,y,z:Point.  (a # b ⇒ x # yz ⇒ aba < xyz)
BY
{ (Auto THEN D 0) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. a # b
8. x # yz
⊢ ¬out(y xz)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. a # b
8. x # yz
⊢ ∃p,p',x',z':Point. (aba ≅a xyp ∧ B(yp'p) ∧ (out(y xx') ∧ out(y zz')) ∧ (¬B(xyp)) ∧ B(x'p'z') ∧ p' # z')

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y,z:Point.    (a  \#  b  {}\mRightarrow{}  x  \#  yz  {}\mRightarrow{}  aba  <  xyz)


By

---

Latex:
(Auto  THEN  D  0)

---

Home Index