---

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


1. e : BasicGeometry
2. A : Point
3. P : Point
4. Q : Point
5. P-AA-Q
⊢ False
BY
{ RepeatFor 3 (D -1) }

1
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)

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  P  :  Point
4.  Q  :  Point
5.  P-AA-Q
\mvdash{}  False


By

---

Latex:
RepeatFor  3  (D  -1)

---

Home Index