---

Step * of Lemma dist-lemma-lt

No Annotations
∀g:EuclideanPlane. ∀a,b,c,d,e,f:Point.  (D(a;b;c;d;e;f) ⇒ |ef| < |ab| + |cd|)
BY
{ ((Auto THEN (FLemma `dist-lemma-le` [-1] THENA Auto) THEN Unfold `geo-lt` 0)
   THEN (Unfold `dist` -2 THEN ExRepD)
   THEN InstConcl [⌜u⌝;⌜c'⌝]⋅
   THEN Auto) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. b' : Point
10. c' : Point
11. u : {u:Point| c' # u} 
12. B(a'b'c')
13. B(a'uc')
14. ab ≅ a'b'
15. cd ≅ b'c'
16. ef ≅ a'u
17. |ef| ≤ |ab| + |cd|
18. u # c'
⊢ |ef| + |uc'| ≤ |ab| + |cd|

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.    (D(a;b;c;d;e;f)  {}\mRightarrow{}  |ef|  <  |ab|  +  |cd|)


By

---

Latex:
((Auto  THEN  (FLemma  `dist-lemma-le`  [-1]  THENA  Auto)  THEN  Unfold  `geo-lt`  0)
  THEN  (Unfold  `dist`  -2  THEN  ExRepD)
  THEN  InstConcl  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index