---

Step * of Lemma geo-opp-side-trivial

∀[e:BasicGeometry]. ∀[A,P,Q:Point].  (¬P-AA-Q)
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. e : BasicGeometry
2. A : Point
3. P : Point
4. Q : Point
5. P-AA-Q
⊢ False

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[A,P,Q:Point].    (\mneg{}P-AA-Q)


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index