---

Step * 1 2 1 1 of Lemma geo-perp-in-iff


1. e : BasicGeometry
2. c : Point
3. d : Point
4. x : Point
5. c ≠ d
⊢ ∃v:Point. (Colinear(c;d;v) ∧ v ≠ x)
BY
{ (Assert ⌜c ≠ x ∨ x ≠ d⌝⋅ THENM (D -1 THEN Auto)) }

1
.....assertion..... 
1. e : BasicGeometry
2. c : Point
3. d : Point
4. x : Point
5. c ≠ d
⊢ c ≠ x ∨ x ≠ d

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  c  :  Point
3.  d  :  Point
4.  x  :  Point
5.  c  \mneq{}  d
\mvdash{}  \mexists{}v:Point.  (Colinear(c;d;v)  \mwedge{}  v  \mneq{}  x)


By

---

Latex:
(Assert  \mkleeneopen{}c  \mneq{}  x  \mvee{}  x  \mneq{}  d\mkleeneclose{}\mcdot{}  THENM  (D  -1  THEN  Auto))

---

Home Index