---

Step * of Lemma left-not-between

∀g:EuclideanPlane. ∀a,b,c:Point.  (a leftof cb ⇒ (¬a_b_c))
BY
{ (Auto THEN (D 0 THENA Auto) THEN (DistinguishCases ⌜b ≠ c⌝⋅ THENA Auto)) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a leftof cb
6. a_b_c
7. b ≠ c
⊢ False

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a leftof cb
6. a_b_c
7. ¬b ≠ c
⊢ False

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c:Point.    (a  leftof  cb  {}\mRightarrow{}  (\mneg{}a\_b\_c))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  (DistinguishCases  \mkleeneopen{}b  \mneq{}  c\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index