---

Step * of Lemma Euclid-drop-perp

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:{c:Point| c # ab} .  (∃p:Point [(Colinear(a;b;p) ∧ ab  ⊥p pc)])
BY
{ (InstLemma `Euclid-drop-perp-1` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN ExRepD
   THEN Auto
   THEN ((InstHyp [⌜c⌝] (-2)⋅ THENA Auto) THENM (D -1 THEN D 0 With ⌜p⌝  THEN Auto))) }

1
.....wf..... 
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. ∀c:{c:Point| ∀x:Point. (Colinear(a;b;x) ⇒ c ≠ x)} . ∃p:Point. (Colinear(a;b;p) ∧ ab  ⊥p pc)
5. c : {c:Point| c # ab} 
⊢ c ∈ {c:Point| ∀x:Point. (Colinear(a;b;x) ⇒ c ≠ x)} 

---

Latex:

---

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


By

---

Latex:
(InstLemma  `Euclid-drop-perp-1`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  ExRepD
  THEN  Auto
  THEN  ((InstHyp  [\mkleeneopen{}c\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THENM  (D  -1  THEN  D  0  With  \mkleeneopen{}p\mkleeneclose{}    THEN  Auto)))

---

Home Index