---

Step * of Lemma interior-implies-lt-angle

No Annotations
∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  (x # yz ⇒ c leftof ba ⇒ (∃f:Point. ((f leftof ba ∧ f leftof cb) ∧ abf ≅a xyz)) ⇒ xyz < abc)
BY
{ ((Auto THEN ExRepD) THEN Unfold `geo-lt-angle` 0) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. x # yz
9. c leftof ba
10. f : Point
11. f leftof ba
12. f leftof cb
13. abf ≅a xyz
⊢ (¬out(b ac))
∧ (∃p,p',x',z':Point. (xyz ≅a abp ∧ B(bp'p) ∧ (out(b ax') ∧ out(b cz')) ∧ (¬B(abp)) ∧ B(x'p'z') ∧ p' # z'))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    (x  \#  yz  {}\mRightarrow{}  c  leftof  ba  {}\mRightarrow{}  (\mexists{}f:Point.  ((f  leftof  ba  \mwedge{}  f  leftof  cb)  \mwedge{}  abf  \mcong{}\msuba{}  xyz))  {}\mRightarrow{}  xyz  <  abc)


By

---

Latex:
((Auto  THEN  ExRepD)  THEN  Unfold  `geo-lt-angle`  0)

---

Home Index