---

Step * 1 1 of Lemma geo-perp-in-not-eq


1. e : BasicGeometry
2. x : Point
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Colinear(a;b;x)
8. Colinear(c;d;x)
9. ∀u,v:Point.  (Colinear(a;b;u) ⇒ Colinear(c;d;v) ⇒ Ruxv)
10. a ≡ b
11. ∀v:Point. (Colinear(c;d;v) ⇒ x ≡ v)
⊢ False
BY
{ ((Assert x ≡ c BY (BHyp -1  THEN Auto)) THEN (Assert x ≡ d BY (BHyp -2  THEN Auto))) }

1
1. e : BasicGeometry
2. x : Point
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Colinear(a;b;x)
8. Colinear(c;d;x)
9. ∀u,v:Point.  (Colinear(a;b;u) ⇒ Colinear(c;d;v) ⇒ Ruxv)
10. a ≡ b
11. ∀v:Point. (Colinear(c;d;v) ⇒ x ≡ v)
12. x ≡ c
13. x ≡ d
⊢ False

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  d  :  Point
7.  Colinear(a;b;x)
8.  Colinear(c;d;x)
9.  \mforall{}u,v:Point.    (Colinear(a;b;u)  {}\mRightarrow{}  Colinear(c;d;v)  {}\mRightarrow{}  Ruxv)
10.  a  \mequiv{}  b
11.  \mforall{}v:Point.  (Colinear(c;d;v)  {}\mRightarrow{}  x  \mequiv{}  v)
\mvdash{}  False


By

---

Latex:
((Assert  x  \mequiv{}  c  BY  (BHyp  -1    THEN  Auto))  THEN  (Assert  x  \mequiv{}  d  BY  (BHyp  -2    THEN  Auto)))

---

Home Index