---

Step * of Lemma geo-triangle-same-line

∀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
{ ((D 0 THENA Auto)
   THEN Assert ⌜∀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)⌝⋅
   ) }

1
.....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)

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)
⊢ ∀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})

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \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:
((D  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\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)\mkleeneclose{}\mcdot{}
  )

---

Home Index