---

Step * 8 of Lemma r2-basic-geo-axioms


∀a,b,c:Point.  (a leftof bc ⇒ b # c)
BY
{ (UnfoldGeoAbbreviations 0 THEN InstLemma `r2-left-sep` [] THEN RepeatFor 4 (ParallelLast') THEN Auto) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. r2-left(a;b;c)
5. b ≠ c
⊢ d(b;b) < d(b;c)

---

Latex:

---

Latex:

\mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  \#  c)


By

---

Latex:
(UnfoldGeoAbbreviations  0
  THEN  InstLemma  `r2-left-sep`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto)

---

Home Index