---

Step * 2 of Lemma Prop22-inequality-implies-triangle


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
BY
{ (ExRepD THEN (CompassCompass2 ⌜a⌝ ⌜c1⌝ ⌜b⌝ ⌜c2⌝ `x' `y'⋅ THENA Auto)) }

1
.....antecedent..... 
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 : Point
9. c2 : Point
10. ac ≅ ac1
11. bc2 > bc1
12. bc ≅ bc2
13. ac1 > ac2
⊢ a # b

2
.....antecedent..... 
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 : Point
9. c2 : Point
10. ac ≅ ac1
11. bc2 > bc1
12. bc ≅ bc2
13. ac1 > ac2
⊢ ∃p,q:Point. ((ac1 ≅ ap ∧ bc2>bp) ∧ bc2 ≅ bq ∧ ac1>aq)

3
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 : Point
9. c2 : Point
10. ac ≅ ac1
11. bc2 > bc1
12. bc ≅ bc2
13. ac1 > ac2
14. x : Point
15. y : Point
16. ax ≅ ac1 ∧ ay ≅ ac1 ∧ bx ≅ bc2 ∧ by ≅ bc2 ∧ x leftof ab ∧ y leftof ba
⊢ a # bc

---

Latex:

---

Latex:

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.  \mexists{}c1,c2:Point.  ((ac  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  bc  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)
\mvdash{}  a  \#  bc


By

---

Latex:
(ExRepD  THEN  (CompassCompass2  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}c1\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c2\mkleeneclose{}  `x'  `y'\mcdot{}  THENA  Auto))

---

Home Index