---

Step * of Lemma geo-between-lt-angle

∀e:EuclideanPlane. ∀a,b,c,p:Point.  (a # bc ⇒ b-p-c ⇒ bap < bac)
BY
{ (Auto THEN Unfold `geo-lt-angle` 0) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a # bc
7. b-p-c
⊢ (¬out(a bc))
∧ (∃p@0,p',x',z':Point. (bap ≅a bap@0 ∧ a_p'_p@0 ∧ (out(a bx') ∧ out(a cz')) ∧ (¬b_a_p@0) ∧ x'_p'_z' ∧ p' ≠ z'))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,p:Point.    (a  \#  bc  {}\mRightarrow{}  b-p-c  {}\mRightarrow{}  bap  <  bac)


By

---

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

---

Home Index