---

Step * 1 of Lemma dist-to-gt


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. D(a;b;b;b;c;d)
⊢ ab > cd
BY
{ (Unfold `dist` -1 THEN Unfold `geo-gt` 0) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ∃a',b',c':Point. ∃u:{u:Point| c' # u} . (B(a'b'c') ∧ B(a'uc') ∧ ab ≅ a'b' ∧ bb ≅ b'c' ∧ cd ≅ a'u)
⊢ ↓∃w:Point. (B(awb) ∧ aw ≅ cd ∧ w # b)

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  D(a;b;b;b;c;d)
\mvdash{}  ab  >  cd


By

---

Latex:
(Unfold  `dist`  -1  THEN  Unfold  `geo-gt`  0)

---

Home Index