---

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


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

1
.....assertion..... 
1. e : BasicGeometry
2. a : Point
3. b : Point
4. x : Point
5. a ≠ b
⊢ a ≠ x ∨ x ≠ b

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  x  :  Point
5.  a  \mneq{}  b
\mvdash{}  \mexists{}u:Point.  (Colinear(a;b;u)  \mwedge{}  u  \mneq{}  x)


By

---

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

---

Home Index