---

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

.....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
BY
{ (FLemma `Dsep-iff-sep` [15] THEN Auto) }

---

Latex:

---

Latex:
.....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.  \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'
25.  x\_y\_z
26.  x'\_y'\_z'
\mvdash{}  x  \mneq{}  y


By

---

Latex:
(FLemma  `Dsep-iff-sep`  [15]  THEN  Auto)

---

Home Index