---

Step * 1 of Lemma geo-triangle-same-line

.....assertion..... 
1. e : HeytingGeometry
⊢ ∀x,a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. ∀d:{d:Point| c ≠ d} .  (line(a;b)=line(c;d) ⇒ x # ab ⇒ x # cd)
BY
{ (Auto THEN DSetVars THEN (Unhide THENA Auto) THEN D -2) }

1
1. e : HeytingGeometry
2. x : Point
3. a : Point
4. b : Point
5. a ≠ b
6. c : Point
7. d : Point
8. c ≠ d
9. Colinear(a;b;c)
10. Colinear(a;b;d)
11. x # ab
⊢ x # cd

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  HeytingGeometry
\mvdash{}  \mforall{}x,a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .  \mforall{}c:Point.  \mforall{}d:\{d:Point|  c  \mneq{}  d\}  .
        (line(a;b)=line(c;d)  {}\mRightarrow{}  x  \#  ab  {}\mRightarrow{}  x  \#  cd)


By

---

Latex:
(Auto  THEN  DSetVars  THEN  (Unhide  THENA  Auto)  THEN  D  -2)

---

Home Index