---

Step * 1 of Lemma geo-line-eq-geoline


1. e : EuclideanPlane
2. P : LINE
3. l : Line
4. fst(l) I P ∧ fst(snd(l)) I P
⊢ l = P ∈ LINE
BY
{ (D 2 THEN EqTypeCD THEN Auto THEN (RWO "-4<" 0 THENA Auto)) }

1
1. e : EuclideanPlane
2. P : Base
3. P1 : Base
4. P = P1 ∈ pertype(λl,m. ((l ∈ Line) ∧ (m ∈ Line) ∧ l ≡ m))
5. P ∈ Line
6. P1 ∈ Line
7. P ≡ P1
8. l : Line
9. fst(l) I P
10. fst(snd(l)) I P
⊢ l ≡ P

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  P  :  LINE
3.  l  :  Line
4.  fst(l)  I  P  \mwedge{}  fst(snd(l))  I  P
\mvdash{}  l  =  P


By

---

Latex:
(D  2  THEN  EqTypeCD  THEN  Auto  THEN  (RWO  "-4<"  0  THENA  Auto))

---

Home Index