---

Step * 1 of Lemma geo-colinear-append


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))))
BY
{ ((Assert (∀C∈L1.Colinear(A;B;C)) BY
          ((RWW "l_all_iff" (-2) THENM RWW "l_all_iff" 0) THEN Auto))
   THEN (Assert (∀C∈L2.Colinear(A;B;C)) BY
               ((RWW "l_all_iff" (-2) THENM RWW "l_all_iff" 0) THEN Auto))
   THEN (Assert (∀C∈L1 @ L2.Colinear(A;B;C)) BY
               (BLemma `l_all_append` THEN Auto))) }

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))))
13. (∀C∈L1.Colinear(A;B;C))
14. (∀C∈L2.Colinear(A;B;C))
15. (∀C∈L1 @ L2.Colinear(A;B;C))
⊢ (∀A∈L1 @ L2.(∀B∈L1 @ L2.(∀C∈L1 @ L2.Colinear(A;B;C))))

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  L1  :  Point  List
3.  L2  :  Point  List
4.  A  :  Point
5.  B  :  Point
6.  A  \mneq{}  B
7.  (A  \mmember{}  L1)
8.  (A  \mmember{}  L2)
9.  (B  \mmember{}  L1)
10.  (B  \mmember{}  L2)
11.  (\mforall{}A\mmember{}L1.(\mforall{}B\mmember{}L1.(\mforall{}C\mmember{}L1.Colinear(A;B;C))))
12.  (\mforall{}A\mmember{}L2.(\mforall{}B\mmember{}L2.(\mforall{}C\mmember{}L2.Colinear(A;B;C))))
\mvdash{}  (\mforall{}A\mmember{}L1  @  L2.(\mforall{}B\mmember{}L1  @  L2.(\mforall{}C\mmember{}L1  @  L2.Colinear(A;B;C))))


By

---

Latex:
((Assert  (\mforall{}C\mmember{}L1.Colinear(A;B;C))  BY
                ((RWW  "l\_all\_iff"  (-2)  THENM  RWW  "l\_all\_iff"  0)  THEN  Auto))
  THEN  (Assert  (\mforall{}C\mmember{}L2.Colinear(A;B;C))  BY
                          ((RWW  "l\_all\_iff"  (-2)  THENM  RWW  "l\_all\_iff"  0)  THEN  Auto))
  THEN  (Assert  (\mforall{}C\mmember{}L1  @  L2.Colinear(A;B;C))  BY
                          (BLemma  `l\_all\_append`  THEN  Auto)))

---

Home Index