---

Step * of Lemma eu-seg-extend_wf

∀[e:EuclideanPlane]. ∀[s:ProperSegment]. ∀[t:Segment].  (s + t ∈ ProperSegment)
BY
{ (ProveWfLemma THEN DVar `s' THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. e : EuclideanPlane
2. s : Segment
3. proper(s)
4. t : Segment
⊢ proper(<s.1, (extend s.1s.2 by t.1t.2)>)

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[s:ProperSegment].  \mforall{}[t:Segment].    (s  +  t  \mmember{}  ProperSegment)


By

---

Latex:
(ProveWfLemma  THEN  DVar  `s'  THEN  MemTypeCD  THEN  Auto)

---

Home Index