---

Step * of Lemma geo-between-out-implies-out

∀e:EuclideanPlane. ∀a,b,c,c':Point.  (out(a cc') ⇒ (a-b-c ∨ a-c-b) ⇒ out(a c'b))
BY
{ (Auto THEN D -1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. c' : Point
6. out(a cc')
7. a-b-c
⊢ out(a c'b)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. c' : Point
6. out(a cc')
7. a-c-b
⊢ out(a c'b)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,c':Point.    (out(a  cc')  {}\mRightarrow{}  (a-b-c  \mvee{}  a-c-b)  {}\mRightarrow{}  out(a  c'b))


By

---

Latex:
(Auto  THEN  D  -1)

---

Home Index