---

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


1. e : HeytingGeometry
2. ∀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)
3. x : Point
4. a : Point
5. b : {b:Point| a ≠ b} 
6. c : Point
7. d : {d:Point| c ≠ d} 
8. line(a;b)=line(c;d)
9. x # ab
⊢ x # cd
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  \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)
3.  x  :  Point
4.  a  :  Point
5.  b  :  \{b:Point|  a  \mneq{}  b\} 
6.  c  :  Point
7.  d  :  \{d:Point|  c  \mneq{}  d\} 
8.  line(a;b)=line(c;d)
9.  x  \#  ab
\mvdash{}  x  \#  cd


By

---

Latex:
Auto

---

Home Index