---

Step * of Lemma geo-add-length-lt-sep

No Annotations
∀e:BasicGeometry. ∀a,b,c,d,g,h:Point.  (|ab| < |cd| + |gh| ⇒ (c # d ∨ g # h))
BY
{ (Auto
   THEN (InstLemma `geo-lt-sep` [⌜e⌝;⌜a⌝;⌜b⌝;⌜X⌝;⌜|cd| + |gh|⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜X⌝;⌜|cd| + |gh|⌝;⌜|cd|⌝]⋅ THENA Auto)
   THEN ParallelLast) }

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

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `geo-lt-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}|cd|  +  |gh|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}|cd|  +  |gh|\mkleeneclose{};\mkleeneopen{}|cd|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast)

---

Home Index