---

Step * of Lemma Euclid-erect-2perp

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:{c:Point| Colinear(a;b;c)} .
  ∃q:Point. (∃p:Point [(ab  ⊥c pc ∧ ab  ⊥c qc ∧ p leftof ab ∧ q leftof ba)])
BY
{ (Auto THEN Assert  ⌜∃d,d':Point. (d ≠ c ∧ d=c=d' ∧ Colinear(a;b;d) ∧ (∀x:Point. (x leftof ab ⇐⇒ x leftof dd')))⌝⋅) }

1
.....assertion..... 
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
⊢ ∃d,d':Point. (d ≠ c ∧ d=c=d' ∧ Colinear(a;b;d) ∧ (∀x:Point. (x leftof ab ⇐⇒ x leftof dd')))

2
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
5. ∃d,d':Point. (d ≠ c ∧ d=c=d' ∧ Colinear(a;b;d) ∧ (∀x:Point. (x leftof ab ⇐⇒ x leftof dd')))
⊢ ∃q:Point. (∃p:Point [(ab  ⊥c pc ∧ ab  ⊥c qc ∧ p leftof ab ∧ q leftof ba)])

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Assert    \mkleeneopen{}\mexists{}d,d':Point
                                (d  \mneq{}  c  \mwedge{}  d=c=d'  \mwedge{}  Colinear(a;b;d)  \mwedge{}  (\mforall{}x:Point.  (x  leftof  ab  \mLeftarrow{}{}\mRightarrow{}  x  leftof  dd')))\mkleeneclose{}\mcdot{}
  )

---

Home Index