---

Step * 1 of Lemma eu-seg-extend_wf

.....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)>)
BY
{ (Assert e ∈ EuclideanPlane BY
         Auto) }

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

---

Latex:

---

Latex:
.....set  predicate..... 
1.  e  :  EuclideanPlane
2.  s  :  Segment
3.  proper(s)
4.  t  :  Segment
\mvdash{}  proper(<s.1,  (extend  s.1s.2  by  t.1t.2)>)


By

---

Latex:
(Assert  e  \mmember{}  EuclideanPlane  BY
              Auto)

---

Home Index