---

Step * of Lemma Prop22-inequality-implies-triangle

No Annotations
∀e:EuclideanPlane. ∀a,b,c:Point.  (|ac| < |ab| + |bc| ⇒ |ab| < |ac| + |bc| ⇒ |bc| < |ac| + |ab| ⇒ a # bc)
BY
{ (Auto THEN Assert ⌜∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)⌝⋅) }

1
.....assertion..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. |ac| < |ab| + |bc|
6. |ab| < |ac| + |bc|
7. |bc| < |ac| + |ab|
⊢ ∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. |ac| < |ab| + |bc|
6. |ab| < |ac| + |bc|
7. |bc| < |ac| + |ab|
8. ∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)
⊢ a # bc

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.
    (|ac|  <  |ab|  +  |bc|  {}\mRightarrow{}  |ab|  <  |ac|  +  |bc|  {}\mRightarrow{}  |bc|  <  |ac|  +  |ab|  {}\mRightarrow{}  a  \#  bc)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mexists{}c1,c2:Point.  ((ac  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  bc  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)\mkleeneclose{}\mcdot{})

---

Home Index