---

Step * 1 of Lemma left-implies-sep


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}
BY
{ ((D 0 THEN Auto) THEN BLemma `geo-sep-sym` THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  leftof  bc
6.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  \mneq{}  c)
7.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  leftof  ca)
8.  b  leftof  ca
9.  c  leftof  ab
10.  a  \mneq{}  b
11.  c  \mneq{}  a
12.  b  \mneq{}  c
\mvdash{}  \{a  \mneq{}  b  \mwedge{}  a  \mneq{}  c  \mwedge{}  b  \mneq{}  c\}


By

---

Latex:
((D  0  THEN  Auto)  THEN  BLemma  `geo-sep-sym`  THEN  Auto)

---

Home Index