---

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

∀e:EuclideanPlane. ∀a,b,x,y,z:Point.  (a ≠ b ⇒ x-y-z ⇒ aba < xyz)
BY
{ (Auto THEN D 0 THEN EAuto 1 THEN InstConcl [⌜x⌝;⌜y⌝;⌜x⌝;⌜z⌝]⋅ THEN EAuto 1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. a ≠ b
8. x-y-z
⊢ aba ≅a xyx

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y,z:Point.    (a  \mneq{}  b  {}\mRightarrow{}  x-y-z  {}\mRightarrow{}  aba  <  xyz)


By

---

Latex:
(Auto  THEN  D  0  THEN  EAuto  1  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index