---

Step * of Lemma Euclid-drop-perp-1

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:{c:Point| ∀x:Point. (Colinear(a;b;x) ⇒ c ≠ x)} .
  ∃p:Point. (Colinear(a;b;p) ∧ ab  ⊥p pc)
BY
{ (InstLemma `Euclid-drop-perp-0` []
   THEN RepeatFor 4 (ParallelLast')
   THEN RepeatFor 2 (D -1)
   THEN D 0 With ⌜p⌝ 
   THEN Auto
   THEN DSetVars
   THEN Unhide
   THEN EAuto 2) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `Euclid-drop-perp-0`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  RepeatFor  2  (D  -1)
  THEN  D  0  With  \mkleeneopen{}p\mkleeneclose{} 
  THEN  Auto
  THEN  DSetVars
  THEN  Unhide
  THEN  EAuto  2)

---

Home Index