---

Step * of Lemma Euclid-Prop6

∀e:EuclideanPlane. ∀a,b,c:Point.  (c # ab ⇒ cab ≅a cba ⇒ ca ≅ cb)
BY
{ Assert ⌜∀e:EuclideanPlane. ∀a,b,c:Point.  (cab ≅a cba ⇒ c leftof ab ⇒ ca ≅ cb)⌝⋅ }

1
.....assertion..... 
∀e:EuclideanPlane. ∀a,b,c:Point.  (cab ≅a cba ⇒ c leftof ab ⇒ ca ≅ cb)

2
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)

---

Latex:

---

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


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (cab  \mcong{}\msuba{}  cba  {}\mRightarrow{}  c  leftof  ab  {}\mRightarrow{}  ca  \mcong{}  cb)\mkleeneclose{}\mcdot{}

---

Home Index