---

Step * 2 1 1 1 1 1 1 1 of Lemma r2-straightedge-compass


1. a : ℝ^2
2. b : ℝ^2
3. q : ℝ^2
4. b ≠ a
5. q_a_b
⊢ q ≠ b
BY
{ ((FLemma `rv-be-dist` [-1] THENA Auto)
   THEN All (Unfold `real-vec-sep`)
   THEN (RWO "real-vec-dist-symmetry" (-3) THENA Auto)) }

1
1. a : ℝ^2
2. b : ℝ^2
3. q : ℝ^2
4. r0 < d(a;b)
5. q_a_b
6. d(q;b) = (d(q;a) + d(a;b))
⊢ r0 < d(q;b)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  q  :  \mBbbR{}\^{}2
4.  b  \mneq{}  a
5.  q\_a\_b
\mvdash{}  q  \mneq{}  b


By

---

Latex:
((FLemma  `rv-be-dist`  [-1]  THENA  Auto)
  THEN  All  (Unfold  `real-vec-sep`)
  THEN  (RWO  "real-vec-dist-symmetry"  (-3)  THENA  Auto))

---

Home Index