---

Step * 1 of Lemma Euclid-Prop6

.....assertion..... 
∀e:EuclideanPlane. ∀a,b,c:Point.  (cab ≅a cba ⇒ c leftof ab ⇒ ca ≅ cb)
BY
{ (Auto
   THEN (InstLemma `Euclid-Prop6-lemma` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA (Auto THEN OrLeft THEN Auto))
   THEN ExRepD
   THEN Thin (-2)
   THEN (D -2 THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. cab ≅a cba
6. c leftof ab
7. x : Point
8. Colinear(c;a;x)
9. ax ≅ bc
10. Cong3(axb,bca)
11. x leftof ab
⊢ ca ≅ cb

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-Prop6-lemma`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  OrLeft  THEN  Auto))
  THEN  ExRepD
  THEN  Thin  (-2)
  THEN  (D  -2  THENA  Auto))

---

Home Index