---

Step * of Lemma colinear-cong3

∀e:EuclideanPlane. ∀a,b,c,x,y:Point.
  (a ≠ b ⇒ Colinear(a;b;c) ⇒ ab ≅ xy ⇒ (∃z:Point. (Colinear(x;y;z) ∧ Cong3(abc,xyz))))
BY
{ (Auto THEN (InstLemma `geo-colinear-sep-cases` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THEN Auto) THEN D -1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. a ≠ b
8. Colinear(a;b;c)
9. ab ≅ xy
10. ¬((¬a_c_b) ∧ (¬a_b_c))
⊢ ∃z:Point. (Colinear(x;y;z) ∧ Cong3(abc,xyz))

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. a ≠ b
8. Colinear(a;b;c)
9. ab ≅ xy
10. ¬((¬b_c_a) ∧ (¬b_a_c))
⊢ ∃z:Point. (Colinear(x;y;z) ∧ Cong3(abc,xyz))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y:Point.
    (a  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  ab  \mcong{}  xy  {}\mRightarrow{}  (\mexists{}z:Point.  (Colinear(x;y;z)  \mwedge{}  Cong3(abc,xyz))))


By

---

Latex:
(Auto  THEN  (InstLemma  `geo-colinear-sep-cases`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1)

---

Home Index