---

Step * 1 1 of Lemma geo-add-length-assoc


1. e : BasicGeometry
2. x : Point
3. B(OXx)
4. y : Point
5. B(OXy)
6. z : Point
7. B(OXz)
8. x1 : Point
9. B(OXx1)
10. y1 : Point
11. B(OXy1)
12. z1 : Point
13. B(OXz1)
14. x ≡ x1
15. y ≡ y1
16. z ≡ z1
17. a : Point
18. B(Oya)
19. ya ≅ Xz
20. ya ≅ Xz
21. B(Oya)
22. b : Point
23. B(Ox1b)
24. x1b ≅ Xy1
25. x1b ≅ Xy1
26. B(Ox1b)
27. c : Point
28. B(Oxc)
29. xc ≅ Xa
30. xc ≅ Xa
31. B(Oxc)
32. B(OXb)
33. B(OXc)
⊢ c = extend Ob by Xz1 ∈ Length
BY
{ (((gEliminatePoint 16 THENA Auto) THEN ThinVar `z' THEN RenameTo `z' `z1')
   THEN ((gEliminatePoint 14 THENA Auto) THEN ThinVar `y' THEN RenameTo `y' `y1')
   THEN (gEliminatePoint 12 THENA Auto)
   THEN ThinVar `x'
   THEN RenameTo `x' `x1') }

1
1. e : BasicGeometry
2. x : Point
3. y : Point
4. z : Point
5. B(OXx)
6. B(OXy)
7. B(OXz)
8. B(OXx)
9. B(OXy)
10. B(OXz)
11. a : Point
12. B(Oya)
13. ya ≅ Xz
14. ya ≅ Xz
15. B(Oya)
16. b : Point
17. B(Oxb)
18. xb ≅ Xy
19. xb ≅ Xy
20. B(Oxb)
21. c : Point
22. B(Oxc)
23. xc ≅ Xa
24. xc ≅ Xa
25. B(Oxc)
26. B(OXb)
27. B(OXc)
⊢ c = extend Ob by Xz ∈ Length

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Point
3.  B(OXx)
4.  y  :  Point
5.  B(OXy)
6.  z  :  Point
7.  B(OXz)
8.  x1  :  Point
9.  B(OXx1)
10.  y1  :  Point
11.  B(OXy1)
12.  z1  :  Point
13.  B(OXz1)
14.  x  \mequiv{}  x1
15.  y  \mequiv{}  y1
16.  z  \mequiv{}  z1
17.  a  :  Point
18.  B(Oya)
19.  ya  \mcong{}  Xz
20.  ya  \mcong{}  Xz
21.  B(Oya)
22.  b  :  Point
23.  B(Ox1b)
24.  x1b  \mcong{}  Xy1
25.  x1b  \mcong{}  Xy1
26.  B(Ox1b)
27.  c  :  Point
28.  B(Oxc)
29.  xc  \mcong{}  Xa
30.  xc  \mcong{}  Xa
31.  B(Oxc)
32.  B(OXb)
33.  B(OXc)
\mvdash{}  c  =  extend  Ob  by  Xz1


By

---

Latex:
(((gEliminatePoint  16  THENA  Auto)  THEN  ThinVar  `z'  THEN  RenameTo  `z'  `z1')
  THEN  ((gEliminatePoint  14  THENA  Auto)  THEN  ThinVar  `y'  THEN  RenameTo  `y'  `y1')
  THEN  (gEliminatePoint  12  THENA  Auto)
  THEN  ThinVar  `x'
  THEN  RenameTo  `x'  `x1')

---

Home Index