---

Step * 5 1 2 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
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)
BY
{ (((OrRight THEN Auto) THEN (InstLemma `Dbet-iff-between` [⌜g⌝;⌜a⌝;⌜d⌝;⌜c⌝]⋅ THEN Auto) THEN D -1 THEN Auto)
   THEN ((((DoubleNegation THENM SupposeMore (-3)) THENA Auto) THEN (RemoveDoubleNegation THENA Auto))
         THEN D -1
         THEN Auto)
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN InstLemma `geo-construction-unicity` [⌜g⌝;⌜a⌝;⌜c⌝;⌜p2⌝;⌜d⌝]⋅
   THEN Auto) }

---

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
15.  p2  :  Point
16.  a-c-p2
17.  cp2  \mcong{}  cd
18.  p1  :  Point
19.  p2-c-p1
20.  cp1  \mcong{}  cd
21.  \mneg{}\mneg{}(B(acd)  \mvee{}  B(adc))
22.  p2  \#  d
\mvdash{}  Dbet(g;a;c;d)  \mvee{}  Dbet(g;a;d;c)


By

---

Latex:
(((OrRight  THEN  Auto)
    THEN  (InstLemma  `Dbet-iff-between`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
    THEN  D  -1
    THEN  Auto)
  THEN  ((((DoubleNegation  THENM  SupposeMore  (-3))  THENA  Auto)  THEN  (RemoveDoubleNegation  THENA  Auto))
              THEN  D  -1
              THEN  Auto)
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  InstLemma  `geo-construction-unicity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index