---

Step * of Lemma eu-inner-pasch-property

∀e:EuclideanPlane
  ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
    (p-eu-inner-pasch(e;a;b;c;p;q)-b ∧ q-eu-inner-pasch(e;a;b;c;p;q)-a)
BY
{ (Auto THEN D 1 THEN Unhide THEN D 2 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  \mneg{}Colinear(a;b;c)\}  ].  \mforall{}[p:\{p:Point|  a-p-c\}  ].  \mforall{}[q:\{q:Point|  b\_q\_c\}  ].
        (p-eu-inner-pasch(e;a;b;c;p;q)-b  \mwedge{}  q-eu-inner-pasch(e;a;b;c;p;q)-a)


By

---

Latex:
(Auto  THEN  D  1  THEN  Unhide  THEN  D  2  THEN  Auto)

---

Home Index