---

Step * of Lemma geo-incident_functionality

∀[e1:EuclideanPlane]. ∀[l,m:Line]. ∀[p,q:Point].  ({uiff(p I l;q I m)}) supposing (p ≡ q and l ≡ m)
BY
{ (Auto
   THEN (Assert l = m ∈ LINE BY
               (EqTypeCD THEN Auto))
   THEN D 0
   THEN RWO "-1" 0
   THEN Auto
   THEN ThinVar `l'
   THEN RepeatFor 3 (ParallelLast)) }

1
1. e1 : EuclideanPlane
2. m : Line
3. p : Point
4. q : Point
5. p ≡ q
6. ∀l:Line. ((l = m ∈ LINE) ⇒ Colinear(p;fst(l);fst(snd(l))))
7. l : Line
8. l = m ∈ LINE
9. Colinear(p;fst(l);fst(snd(l)))
⊢ Colinear(q;fst(l);fst(snd(l)))

2
1. e1 : EuclideanPlane
2. m : Line
3. p : Point
4. q : Point
5. p ≡ q
6. ∀l:Line. ((l = m ∈ LINE) ⇒ Colinear(q;fst(l);fst(snd(l))))
7. l : Line
8. l = m ∈ LINE
9. Colinear(q;fst(l);fst(snd(l)))
⊢ Colinear(p;fst(l);fst(snd(l)))

---

Latex:

---

Latex:
\mforall{}[e1:EuclideanPlane].  \mforall{}[l,m:Line].  \mforall{}[p,q:Point].    (\{uiff(p  I  l;q  I  m)\})  supposing  (p  \mequiv{}  q  and  l  \mequiv{}  m)


By

---

Latex:
(Auto
  THEN  (Assert  l  =  m  BY
                          (EqTypeCD  THEN  Auto))
  THEN  D  0
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  ThinVar  `l'
  THEN  RepeatFor  3  (ParallelLast))

---

Home Index