---

Step * 1 1 of Lemma geo-opp-side-trivial


1. e : BasicGeometry
2. A : Point
3. P : Point
4. Q : Point
5. ¬(∀T:Point. (P_T_Q ⇒ (¬Colinear(A;A;T))))
6. ¬Colinear(A;A;P)
⊢ Colinear(A;A;Q)
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  P  :  Point
4.  Q  :  Point
5.  \mneg{}(\mforall{}T:Point.  (P\_T\_Q  {}\mRightarrow{}  (\mneg{}Colinear(A;A;T))))
6.  \mneg{}Colinear(A;A;P)
\mvdash{}  Colinear(A;A;Q)


By

---

Latex:
Auto

---

Home Index