---

Step * of Lemma left-implies-sep

∀g:EuclideanPlane. ∀a,b,c:Point.  (a leftof bc ⇒ {a ≠ b ∧ a ≠ c ∧ b ≠ c})
BY
{ (Auto
   THEN (Assert (∀a,b,c:Point.  (a leftof bc ⇒ b ≠ c)) ∧ (∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)) BY
               (UseEuAxioms THEN Auto))
   THEN D -1
   THEN (FHyp (-1) [5] THENA Auto)
   THEN (FHyp (-2) [-1] THENA Auto)
   THEN ∀h:hyp. (FHyp 6 [h] THENA Auto) ) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a leftof bc
6. ∀a,b,c:Point.  (a leftof bc ⇒ b ≠ c)
7. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
8. b leftof ca
9. c leftof ab
10. a ≠ b
11. c ≠ a
12. b ≠ c
⊢ {a ≠ b ∧ a ≠ c ∧ b ≠ c}

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  \{a  \mneq{}  b  \mwedge{}  a  \mneq{}  c  \mwedge{}  b  \mneq{}  c\})


By

---

Latex:
(Auto
  THEN  (Assert  (\mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  \mneq{}  c))
                          \mwedge{}  (\mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  leftof  ca))  BY
                          (UseEuAxioms  THEN  Auto))
  THEN  D  -1
  THEN  (FHyp  (-1)  [5]  THENA  Auto)
  THEN  (FHyp  (-2)  [-1]  THENA  Auto)
  THEN  \mforall{}h:hyp.  (FHyp  6  [h]  THENA  Auto)  )

---

Home Index