---

Step * of Lemma Euclid-drop-perp-00

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point.  ∃x,p:Point. (Colinear(p;x;c) ∧ ab  ⊥p px ∧ x # ab ∧ x ≠ c)
BY
{ (InstLemma `Euclid-drop-perp-0-ext` [] THEN RepeatFor 6 (ParallelLast') THEN Auto THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .  \mforall{}c:Point.
    \mexists{}x,p:Point.  (Colinear(p;x;c)  \mwedge{}  ab    \mbot{}p  px  \mwedge{}  x  \#  ab  \mwedge{}  x  \mneq{}  c)


By

---

Latex:
(InstLemma  `Euclid-drop-perp-0-ext`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Auto
  THEN  Unhide
  THEN  Auto)

---

Home Index