---

Step * of Lemma Euclid-erect-perp-on-same-side

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:{c:Point| Colinear(a;b;c)} . ∀q:{q:Point| q # ab} .
  (∃p:Point [(ab  ⊥c pc ∧ p # ab ∧ (p leftof ab ⇐⇒ q leftof ab))])
BY
{ (Auto
   THEN (Assert q # ab BY
               Auto)
   THEN (InstLemma `Euclid-erect-2perp` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D -1)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
5. q : {q:Point| q # ab} 
6. q # ab
7. q1 : Point
8. p : Point
9. [%4] : ab  ⊥c pc ∧ ab  ⊥c q1c ∧ p leftof ab ∧ q1 leftof ba
⊢ ∃p:Point [(ab  ⊥c pc ∧ p # ab ∧ (p leftof ab ⇐⇒ q leftof ab))]

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  q  \#  ab  BY
                          Auto)
  THEN  (InstLemma  `Euclid-erect-2perp`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1))

---

Home Index