---

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


1. e : BasicGeometry
2. x : Point
3. B(OXx)
4. y : Point
5. B(OXy)
6. x1 : Point
7. B(OXx1)
8. y1 : Point
9. B(OXy1)
10. x ≡ x1
11. y ≡ y1
12. a : Point
13. B(Oxa)
14. xa ≅ Xy
15. xa ≅ Xy
16. B(Oxa)
17. b : Point
18. B(Oy1b)
19. y1b ≅ Xx1
20. y1b ≅ Xx1
21. B(Oy1b)
⊢ a ≡ b
BY
{ (((gEliminatePoint 10 THENA Auto) THEN ThinVar `x' THEN RenameTo `x' `x1')
   THEN (gEliminatePoint 9 THENA Auto)
   THEN ThinVar `y'
   THEN RenameTo `y' `y1') }

1
1. e : BasicGeometry
2. y : Point
3. x : Point
4. B(OXx)
5. B(OXy)
6. B(OXx)
7. B(OXy)
8. a : Point
9. B(Oxa)
10. xa ≅ Xy
11. xa ≅ Xy
12. B(Oxa)
13. b : Point
14. B(Oyb)
15. yb ≅ Xx
16. yb ≅ Xx
17. B(Oyb)
⊢ a ≡ b

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Point
3.  B(OXx)
4.  y  :  Point
5.  B(OXy)
6.  x1  :  Point
7.  B(OXx1)
8.  y1  :  Point
9.  B(OXy1)
10.  x  \mequiv{}  x1
11.  y  \mequiv{}  y1
12.  a  :  Point
13.  B(Oxa)
14.  xa  \mcong{}  Xy
15.  xa  \mcong{}  Xy
16.  B(Oxa)
17.  b  :  Point
18.  B(Oy1b)
19.  y1b  \mcong{}  Xx1
20.  y1b  \mcong{}  Xx1
21.  B(Oy1b)
\mvdash{}  a  \mequiv{}  b


By

---

Latex:
(((gEliminatePoint  10  THENA  Auto)  THEN  ThinVar  `x'  THEN  RenameTo  `x'  `x1')
  THEN  (gEliminatePoint  9  THENA  Auto)
  THEN  ThinVar  `y'
  THEN  RenameTo  `y'  `y1')

---

Home Index