---

Step * of Lemma geo-colinear-append

∀e:EuclideanPlane. ∀L1,L2:Point List.
  ((∃A,B:Point. (A ≠ B ∧ ((A ∈ L1) ∧ (A ∈ L2)) ∧ (B ∈ L1) ∧ (B ∈ L2)))
  ⇒ geo-colinear-set(e; L1)
  ⇒ geo-colinear-set(e; L2)
  ⇒ geo-colinear-set(e; L1 @ L2))
BY
{ (Auto THEN ExRepD THEN All (Unfold `geo-colinear-set`)) }

1
1. e : EuclideanPlane
2. L1 : Point List
3. L2 : Point List
4. A : Point
5. B : Point
6. A ≠ B
7. (A ∈ L1)
8. (A ∈ L2)
9. (B ∈ L1)
10. (B ∈ L2)
11. (∀A∈L1.(∀B∈L1.(∀C∈L1.Colinear(A;B;C))))
12. (∀A∈L2.(∀B∈L2.(∀C∈L2.Colinear(A;B;C))))
⊢ (∀A∈L1 @ L2.(∀B∈L1 @ L2.(∀C∈L1 @ L2.Colinear(A;B;C))))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}L1,L2:Point  List.
    ((\mexists{}A,B:Point.  (A  \mneq{}  B  \mwedge{}  ((A  \mmember{}  L1)  \mwedge{}  (A  \mmember{}  L2))  \mwedge{}  (B  \mmember{}  L1)  \mwedge{}  (B  \mmember{}  L2)))
    {}\mRightarrow{}  geo-colinear-set(e;  L1)
    {}\mRightarrow{}  geo-colinear-set(e;  L2)
    {}\mRightarrow{}  geo-colinear-set(e;  L1  @  L2))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  All  (Unfold  `geo-colinear-set`))

---

Home Index