---

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


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. zu ≅ z'u'
⊢ Dcong(e;z;u;z';u')
BY
{ (FLemma `Dcong-iff-cong` [-1] THEN Auto) }

---

Latex:

---

Latex:

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.  zu  \mcong{}  z'u'
\mvdash{}  Dcong(e;z;u;z';u')


By

---

Latex:
(FLemma  `Dcong-iff-cong`  [-1]  THEN  Auto)

---

Home Index