---

Step * 2 2 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 # cd
⊢ x # ab
BY
{ (Assert line(c;d)=line(a;b) BY
         EAuto 1) }

1
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 # cd
10. line(c;d)=line(a;b)
⊢ x # ab

---

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  \#  cd
\mvdash{}  x  \#  ab


By

---

Latex:
(Assert  line(c;d)=line(a;b)  BY
              EAuto  1)

---

Home Index