---

Step * of Lemma zero-angle-less-than-all

∀g:EuclideanPlane. ∀a,b,x,y,z:Point.  (a ≠ b ⇒ x # yz ⇒ aba < xyz)
BY
{ (Auto
   THEN (InstLemma `zero-angles-congruent` [⌜g⌝;⌜a⌝;⌜b⌝;⌜a⌝;⌜x⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto)
   THEN (ExRepD THEN Unfold `geo-lt-angle` 0)
   THEN D 0) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. a ≠ b
8. x # yz
9. aba ≅a xyx
⊢ ¬out(y xz)

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. a ≠ b
8. x # yz
9. aba ≅a xyx
⊢ ∃p,p',x',z':Point. (aba ≅a xyp ∧ y_p'_p ∧ (out(y xx') ∧ out(y zz')) ∧ (¬x_y_p) ∧ x'_p'_z' ∧ p' ≠ z')

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `zero-angles-congruent`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ExRepD  THEN  Unfold  `geo-lt-angle`  0)
  THEN  D  0)

---

Home Index