---

Step * of Lemma perp-col

∀e:BasicGeometry. ∀a,b,c,d,x,y:Point.  (a ≠ b ⇒ ab  ⊥x cd ⇒ x ≠ y ⇒ Colinear(a;b;x) ⇒ Colinear(a;b;y) ⇒ cd  ⊥x xy)
BY
{ (((Auto THEN Unfold `geo-perp-in` 9) THEN ExRepD) THEN Assert ⌜Colinear(a;x;y)⌝⋅) }

1
.....assertion..... 
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)
⊢ Colinear(a;x;y)

2
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)
⊢ cd  ⊥x xy

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d,x,y:Point.
    (a  \mneq{}  b  {}\mRightarrow{}  ab    \mbot{}x  cd  {}\mRightarrow{}  x  \mneq{}  y  {}\mRightarrow{}  Colinear(a;b;x)  {}\mRightarrow{}  Colinear(a;b;y)  {}\mRightarrow{}  cd    \mbot{}x  xy)


By

---

Latex:
(((Auto  THEN  Unfold  `geo-perp-in`  9)  THEN  ExRepD)  THEN  Assert  \mkleeneopen{}Colinear(a;x;y)\mkleeneclose{}\mcdot{})

---

Home Index