---

Step * of Lemma geo-triangle-inequality-lt-sep

∀e:BasicGeometry. ∀a,b,c,d,g,h:Point.
  (|ab| < |gh| + |cd| ⇒ |cd| < |ab| + |gh| ⇒ |gh| < |cd| + |ab| ⇒ ((a ≠ b ∧ g ≠ h) ∧ c ≠ d))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. g : Point
7. h : Point
8. |ab| < |gh| + |cd|
9. |cd| < |ab| + |gh|
10. |gh| < |cd| + |ab|
⊢ a ≠ b

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. g : Point
7. h : Point
8. |ab| < |gh| + |cd|
9. |cd| < |ab| + |gh|
10. |gh| < |cd| + |ab|
11. a ≠ b
⊢ g ≠ h

3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. g : Point
7. h : Point
8. |ab| < |gh| + |cd|
9. |cd| < |ab| + |gh|
10. |gh| < |cd| + |ab|
11. a ≠ b
12. g ≠ h
⊢ c ≠ d

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d,g,h:Point.
    (|ab|  <  |gh|  +  |cd|  {}\mRightarrow{}  |cd|  <  |ab|  +  |gh|  {}\mRightarrow{}  |gh|  <  |cd|  +  |ab|  {}\mRightarrow{}  ((a  \mneq{}  b  \mwedge{}  g  \mneq{}  h)  \mwedge{}  c  \mneq{}  d))


By

---

Latex:
Auto

---

Home Index