---

Step * 2 1 of Lemma perp-col


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. a ≠ b
9. Colinear(a;b;x)
10. Colinear(c;d;x)
11. ∀u,v:Point.  (Colinear(a;b;u) ⇒ Colinear(c;d;v) ⇒ Ruxv)
12. x ≠ y
13. Colinear(a;b;x)
14. Colinear(a;b;y)
15. Colinear(a;x;y)
16. Colinear(x;y;x)
17. u : Point
18. v : Point
19. Colinear(c;d;u)
20. Colinear(x;y;v)
⊢ Ruxv
BY
{ (InstHyp [⌜v⌝;⌜u⌝] 11⋅ THENA Auto) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. a ≠ b
9. Colinear(a;b;x)
10. Colinear(c;d;x)
11. ∀u,v:Point.  (Colinear(a;b;u) ⇒ Colinear(c;d;v) ⇒ Ruxv)
12. x ≠ y
13. Colinear(a;b;x)
14. Colinear(a;b;y)
15. Colinear(a;x;y)
16. Colinear(x;y;x)
17. u : Point
18. v : Point
19. Colinear(c;d;u)
20. Colinear(x;y;v)
21. Rvxu
⊢ Ruxv

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  x  :  Point
7.  y  :  Point
8.  a  \mneq{}  b
9.  Colinear(a;b;x)
10.  Colinear(c;d;x)
11.  \mforall{}u,v:Point.    (Colinear(a;b;u)  {}\mRightarrow{}  Colinear(c;d;v)  {}\mRightarrow{}  Ruxv)
12.  x  \mneq{}  y
13.  Colinear(a;b;x)
14.  Colinear(a;b;y)
15.  Colinear(a;x;y)
16.  Colinear(x;y;x)
17.  u  :  Point
18.  v  :  Point
19.  Colinear(c;d;u)
20.  Colinear(x;y;v)
\mvdash{}  Ruxv


By

---

Latex:
(InstHyp  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  11\mcdot{}  THENA  Auto)

---

Home Index