---

Step * of Lemma Euclid-Prop6-lemma

No Annotations
∀e:EuclideanPlane. ∀a,b,c:Point.
  (cab ≅a cba
  ⇒ c # ab
  ⇒ (∃x:Point
       (Colinear(c;a;x) ∧ ax ≅ bc ∧ (c leftof ab ⇒ x leftof ab) ∧ (c leftof ba ⇒ x leftof ba) ∧ Cong3(axb,bca))))
BY
{ (Auto THEN (InstLemma `Euclid-Prop2` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto) THEN D -1 THEN RenameVar `u' (-2)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. cab ≅a cba
6. c # ab
7. u : Point
8. [%8] : au ≅ bc
⊢ ∃x:Point. (Colinear(c;a;x) ∧ ax ≅ bc ∧ (c leftof ab ⇒ x leftof ab) ∧ (c leftof ba ⇒ x leftof ba) ∧ Cong3(axb,bca))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.
    (cab  \mcong{}\msuba{}  cba
    {}\mRightarrow{}  c  \#  ab
    {}\mRightarrow{}  (\mexists{}x:Point
              (Colinear(c;a;x)
              \mwedge{}  ax  \mcong{}  bc
              \mwedge{}  (c  leftof  ab  {}\mRightarrow{}  x  leftof  ab)
              \mwedge{}  (c  leftof  ba  {}\mRightarrow{}  x  leftof  ba)
              \mwedge{}  Cong3(axb,bca))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-Prop2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `u'  (-2))

---

Home Index