---

Step * of Lemma eu-colinear-append

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

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

---

Latex:

---

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


By

---

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

---

Home Index