---

Step * 5 1 of Lemma eu-eq_dist-axiomsB


1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Dbet(g;a;b;c)
8. Dbet(g;a;b;d)
9. Dsep(g;a;b)
10. Dsep(g;c;d)
11. B(abc)
12. B(abd)
13. a # b
14. c # d
⊢ Dbet(g;a;c;d) ∨ Dbet(g;a;d;c)
BY
{ (((gProperProlong ⌜a⌝⌜c⌝`p2'⌜c⌝⌜d⌝⋅ THEN Auto) THEN gProperProlong ⌜p2⌝⌜c⌝`p1'⌜c⌝⌜d⌝⋅ THEN Auto)
   THEN (Assert ¬¬(B(acd) ∨ B(adc)) BY
               ((Assert (¬((¬B(acd)) ∧ (¬B(adc)))) ⇒ (¬¬(B(acd) ∨ B(adc))) BY
                       Auto)
                THEN InstLemma `geo-between-same-side` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅
                THEN Auto))
   THEN (InstLemma `geo-sep-or` [⌜g⌝;⌜p1⌝;⌜p2⌝;⌜d⌝]⋅ THEN Auto)
   THEN D -1) }

1
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Dbet(g;a;b;c)
8. Dbet(g;a;b;d)
9. Dsep(g;a;b)
10. Dsep(g;c;d)
11. B(abc)
12. B(abd)
13. a # b
14. c # d
15. p2 : Point
16. a-c-p2
17. cp2 ≅ cd
18. p1 : Point
19. p2-c-p1
20. cp1 ≅ cd
21. ¬¬(B(acd) ∨ B(adc))
22. p1 # d
⊢ Dbet(g;a;c;d) ∨ Dbet(g;a;d;c)

2
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Dbet(g;a;b;c)
8. Dbet(g;a;b;d)
9. Dsep(g;a;b)
10. Dsep(g;c;d)
11. B(abc)
12. B(abd)
13. a # b
14. c # d
15. p2 : Point
16. a-c-p2
17. cp2 ≅ cd
18. p1 : Point
19. p2-c-p1
20. cp1 ≅ cd
21. ¬¬(B(acd) ∨ B(adc))
22. p2 # d
⊢ Dbet(g;a;c;d) ∨ Dbet(g;a;d;c)

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  |ac|  <  |ab|  +  |bc|)
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  d  :  Point
7.  Dbet(g;a;b;c)
8.  Dbet(g;a;b;d)
9.  Dsep(g;a;b)
10.  Dsep(g;c;d)
11.  B(abc)
12.  B(abd)
13.  a  \#  b
14.  c  \#  d
\mvdash{}  Dbet(g;a;c;d)  \mvee{}  Dbet(g;a;d;c)


By

---

Latex:
(((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`p2'\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  gProperProlong  \mkleeneopen{}p2\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`p1'\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  \mneg{}\mneg{}(B(acd)  \mvee{}  B(adc))  BY
                          ((Assert  (\mneg{}((\mneg{}B(acd))  \mwedge{}  (\mneg{}B(adc))))  {}\mRightarrow{}  (\mneg{}\mneg{}(B(acd)  \mvee{}  B(adc)))  BY
                                          Auto)
                            THEN  InstLemma  `geo-between-same-side`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  D  -1)

---

Home Index