---

Step * 1 of Lemma eu-eq_dist-axiomsC-five-segment

.....assertion..... 
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. x' : Point
6. y' : Point
7. z' : Point
8. u : Point
9. u' : Point
10. Dcong(e;x;y;x';y')
11. Dcong(e;y;z;y';z')
12. Dcong(e;x;u;x';u')
13. Dcong(e;y;u;y';u')
14. Dbet(e;x;y;z)
15. Dsep(e;x;y)
16. Dsep(e;y;z)
17. Dbet(e;x';y';z')
18. Dsep(e;x';y')
19. Dsep(e;y';z')
20. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
21. xy ≅ x'y'
22. yz ≅ y'z'
23. xu ≅ x'u'
24. yu ≅ y'u'
⊢ zu ≅ z'u'
BY
{ (((FLemma `Dbet-to-between` [14] THEN Auto) THEN FLemma `Dbet-to-between` [17] THEN Auto)
   THEN InstLemma `geo-five-segment` [⌜e⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜u⌝;⌜x'⌝;⌜y'⌝;⌜z'⌝;⌜u'⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. x' : Point
6. y' : Point
7. z' : Point
8. u : Point
9. u' : Point
10. Dcong(e;x;y;x';y')
11. Dcong(e;y;z;y';z')
12. Dcong(e;x;u;x';u')
13. Dcong(e;y;u;y';u')
14. Dbet(e;x;y;z)
15. Dsep(e;x;y)
16. Dsep(e;y;z)
17. Dbet(e;x';y';z')
18. Dsep(e;x';y')
19. Dsep(e;y';z')
20. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
21. xy ≅ x'y'
22. yz ≅ y'z'
23. xu ≅ x'u'
24. yu ≅ y'u'
25. x_y_z
26. x'_y'_z'
⊢ x ≠ y

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanPlane
2.  x  :  Point
3.  y  :  Point
4.  z  :  Point
5.  x'  :  Point
6.  y'  :  Point
7.  z'  :  Point
8.  u  :  Point
9.  u'  :  Point
10.  Dcong(e;x;y;x';y')
11.  Dcong(e;y;z;y';z')
12.  Dcong(e;x;u;x';u')
13.  Dcong(e;y;u;y';u')
14.  Dbet(e;x;y;z)
15.  Dsep(e;x;y)
16.  Dsep(e;y;z)
17.  Dbet(e;x';y';z')
18.  Dsep(e;x';y')
19.  Dsep(e;y';z')
20.  \mforall{}A,B,C:Point.    (A  \#  BC  {}\mRightarrow{}  |AC|  <  |AB|  +  |BC|)
21.  xy  \mcong{}  x'y'
22.  yz  \mcong{}  y'z'
23.  xu  \mcong{}  x'u'
24.  yu  \mcong{}  y'u'
\mvdash{}  zu  \mcong{}  z'u'


By

---

Latex:
(((FLemma  `Dbet-to-between`  [14]  THEN  Auto)  THEN  FLemma  `Dbet-to-between`  [17]  THEN  Auto)
  THEN  InstLemma  `geo-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}u'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index