---

Step * of Lemma oriented-colinear-append

∀e:OrientedPlane. ∀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
{ (InstLemma `geo-colinear-append` [] THEN NthHypSq (-1) THEN EqCD THEN Auto THEN ByComputation 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:OrientedPlane.  \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:
(InstLemma  `geo-colinear-append`  []
  THEN  NthHypSq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  ByComputation  0
  THEN  Auto)

---

Home Index