---

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


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
BY
{ ((RepeatFor 2 (MoveToConcl (-1)) THEN (GenConcl ⌜P = m ∈ Line⌝⋅ THENA Auto)) THEN All Thin⋅) }

1
1. e : EuclideanPlane
2. l : Line
3. m : Line
⊢ fst(l) I m ⇒ fst(snd(l)) I m ⇒ l ≡ m

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  P  :  Base
3.  P1  :  Base
4.  P  =  P1
5.  P  \mmember{}  Line
6.  P1  \mmember{}  Line
7.  P  \mequiv{}  P1
8.  l  :  Line
9.  fst(l)  I  P
10.  fst(snd(l))  I  P
\mvdash{}  l  \mequiv{}  P


By

---

Latex:
((RepeatFor  2  (MoveToConcl  (-1))  THEN  (GenConcl  \mkleeneopen{}P  =  m\mkleeneclose{}\mcdot{}  THENA  Auto))  THEN  All  Thin\mcdot{})

---

Home Index