---

Step * 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)
⊢ ∀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 (RepeatFor 2 (D 0) THENA Auto)) }

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 # ab
⊢ x # cd

2
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

---

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)
\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  \mLeftarrow{}{}\mRightarrow{}  x  \#  cd\})


By

---

Latex:
(Auto  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index