---

Step * 2 of Lemma Euclid-Prop6


1. ∀e:EuclideanPlane. ∀a,b,c:Point.  (cab ≅a cba ⇒ c leftof ab ⇒ ca ≅ cb)
⊢ ∀e:EuclideanPlane. ∀a,b,c:Point.  (c # ab ⇒ cab ≅a cba ⇒ ca ≅ cb)
BY
{ (Auto THEN (D -2 THENL [(BHyp 1 THEN Auto); ((Assert cb ≅ ca BY (BHyp 1 THEN EAuto 1)) THEN Auto)])) }

---

Latex:

---

Latex:

1.  \mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (cab  \mcong{}\msuba{}  cba  {}\mRightarrow{}  c  leftof  ab  {}\mRightarrow{}  ca  \mcong{}  cb)
\mvdash{}  \mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (c  \#  ab  {}\mRightarrow{}  cab  \mcong{}\msuba{}  cba  {}\mRightarrow{}  ca  \mcong{}  cb)


By

---

Latex:
(Auto  THEN  (D  -2  THENL  [(BHyp  1  THEN  Auto);  ((Assert  cb  \mcong{}  ca  BY  (BHyp  1  THEN  EAuto  1))  THEN  Auto)]))

---

Home Index