---

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

∀e:EuclideanPlane. ∀a,b,c,c':Point.  (out(a cc') ⇒ ((a_b_c ∧ a ≠ b) ∨ (a_c_b ∧ a ≠ c)) ⇒ 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 ∧ a ≠ b
⊢ 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 ∧ a ≠ c
⊢ out(a c'b)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  -1)

---

Home Index