---

Step * 1 1 of Lemma eu-colinear-append


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))))
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.(¬(A = B ∈ Point)) ⇒ Colinear(A;B;C))))
BY
{ ((RWO "l_all_iff" (-1) THENA Auto)
   THEN (RWW "l_all_iff" 0 THEN Auto)
   THEN (Assert Colinear(A;B;A1) ∧ Colinear(A;B;B1) ∧ Colinear(A;B;C) BY
               Auto)) }

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))))
13. (∀C∈L1.Colinear(A;B;C))
14. (∀C∈L2.Colinear(A;B;C))
15. ∀C:Point. ((C ∈ L1 @ L2) ⇒ Colinear(A;B;C))
16. A1 : Point
17. (A1 ∈ L1 @ L2)
18. B1 : Point
19. (B1 ∈ L1 @ L2)
20. C : Point
21. (C ∈ L1 @ L2)
22. ¬(A1 = B1 ∈ Point)
23. Colinear(A;B;A1) ∧ Colinear(A;B;B1) ∧ Colinear(A;B;C)
⊢ Colinear(A1;B1;C)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  L1  :  Point  List
3.  L2  :  Point  List
4.  A  :  Point
5.  B  :  Point
6.  \mneg{}(A  =  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.(\mneg{}(A  =  B))  {}\mRightarrow{}  Colinear(A;B;C))))
12.  (\mforall{}A\mmember{}L2.(\mforall{}B\mmember{}L2.(\mforall{}C\mmember{}L2.(\mneg{}(A  =  B))  {}\mRightarrow{}  Colinear(A;B;C))))
13.  (\mforall{}C\mmember{}L1.Colinear(A;B;C))
14.  (\mforall{}C\mmember{}L2.Colinear(A;B;C))
15.  (\mforall{}C\mmember{}L1  @  L2.Colinear(A;B;C))
\mvdash{}  (\mforall{}A\mmember{}L1  @  L2.(\mforall{}B\mmember{}L1  @  L2.(\mforall{}C\mmember{}L1  @  L2.(\mneg{}(A  =  B))  {}\mRightarrow{}  Colinear(A;B;C))))


By

---

Latex:
((RWO  "l\_all\_iff"  (-1)  THENA  Auto)
  THEN  (RWW  "l\_all\_iff"  0  THEN  Auto)
  THEN  (Assert  Colinear(A;B;A1)  \mwedge{}  Colinear(A;B;B1)  \mwedge{}  Colinear(A;B;C)  BY
                          Auto))

---

Home Index