---

Step * of Lemma geo-line-eq-geoline

∀[e:EuclideanPlane]. ∀[P:LINE]. ∀[l:Line].  uiff(fst(l) I P ∧ fst(snd(l)) I P;l = P ∈ LINE)
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA (Auto THEN SubsumeC ⌜Line⌝⋅ THEN Auto))) }

1
1. e : EuclideanPlane
2. P : LINE
3. l : Line
4. fst(l) I P ∧ fst(snd(l)) I P
⊢ l = P ∈ LINE

2
1. e : EuclideanPlane
2. P : LINE
3. l : Line
4. l = P ∈ LINE
⊢ fst(l) I P ∧ fst(snd(l)) I P

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[P:LINE].  \mforall{}[l:Line].    uiff(fst(l)  I  P  \mwedge{}  fst(snd(l))  I  P;l  =  P)


By

---

Latex:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}Line\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index