---

Step * 1 of Lemma Euclid-erect-2perp

.....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')))
BY
{ ((Assert a ≠ b BY
          Auto)
   THEN DVar `b'
   THEN Thin 4
   THEN (Assert Colinear(a;b;c) BY
               Auto)
   THEN DVar `c'
   THEN Thin 5
   THEN (InstLemma `geo-colinear-sep-cases` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
   THEN D -1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. Colinear(a;b;c)
7. ¬((¬a_c_b) ∧ (¬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 : Point
4. c : Point
5. a ≠ b
6. Colinear(a;b;c)
7. ¬((¬b_c_a) ∧ (¬b_a_c))
⊢ ∃d,d':Point. (d ≠ c ∧ d=c=d' ∧ Colinear(a;b;d) ∧ (∀x:Point. (x leftof ab ⇐⇒ x leftof dd')))

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \mneq{}  b\} 
4.  c  :  \{c:Point|  Colinear(a;b;c)\} 
\mvdash{}  \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')))


By

---

Latex:
((Assert  a  \mneq{}  b  BY
                Auto)
  THEN  DVar  `b'
  THEN  Thin  4
  THEN  (Assert  Colinear(a;b;c)  BY
                          Auto)
  THEN  DVar  `c'
  THEN  Thin  5
  THEN  (InstLemma  `geo-colinear-sep-cases`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index