---

Step * 1 1 of Lemma eu-seg-extend_wf


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)>)
BY
{ ((DVar `s' THEN DVar `t')
   THEN All (RepUR ``eu-seg-proper eu-seg1 eu-seg2``)
   THEN (D 0 THENA Auto)
   THEN D 1
   THEN D 2
   THEN ExRepD) }

1
1. e : EuclideanStructure
2. ∀[a,b:Point].  ab=ba
3. ∀[a,b,p,q,r,s:Point].  (pq=rs) supposing (ab=rs and ab=pq)
4. ∀[a,b,c:Point].  a = b ∈ Point supposing ab=cc
5. ∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point].  (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)
6. ∀[a,b,c,d,A,B,C,D:Point].
     (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))
7. ∀[a,b:Point].  (¬a-b-a)
8. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
     let x = eu-inner-pasch(e;a;b;c;p;q) in
         p-x-b ∧ q-x-a
9. ∀[a,b,p,q,r:Point].  (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (¬(a = b ∈ Point)))
10. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ].  let x = middle(a;b;c) in ax=bx ∧ ax=cx
11. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point| 
                                                                                            aq=ay
                                                                                            ∧ (¬(q = p ∈ Point))} ].
      let uv = intersect pq (at radius xy) with Oab  in
          afst(uv)=ab
          ∧ asnd(uv)=ab
          ∧ p_fst(uv)_q
          ∧ snd(uv)_p_q
          ∧ ¬((fst(uv)) = (snd(uv)) ∈ Point) supposing ¬(x = b ∈ Point)
12. ∀[a,b,c:Point].  c-b-a supposing a-b-c
13. ∀[a,b,c,d:Point].  (a-b-c) supposing (b-c-d and a-b-d)
14. s1 : Point
15. s2 : Point
16. ¬(s1 = s2 ∈ Point)
17. t1 : Point
18. t2 : Point
19. e ∈ EuclideanPlane
20. s1 = (extend s1s2 by t1t2) ∈ Point
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
((DVar  `s'  THEN  DVar  `t')
  THEN  All  (RepUR  ``eu-seg-proper  eu-seg1  eu-seg2``)
  THEN  (D  0  THENA  Auto)
  THEN  D  1
  THEN  D  2
  THEN  ExRepD)

---

Home Index