---

Step * 1 1 of Lemma geo-gt-trans


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. w1 : Point
9. a_w1_b
10. aw1 ≅ cd
11. w1 ≠ b
12. w : Point
13. c_w_d
14. cw ≅ xy
15. w ≠ d
16. b' : Point
17. a_b'_w1
18. cw ≅ ab'
19. wd ≅ b'w1
20. a_b'_b
21. ab' ≅ xy
⊢ b' ≠ b
BY
{ ((Assert b'_w1_b BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  x  :  Point
7.  y  :  Point
8.  w1  :  Point
9.  a\_w1\_b
10.  aw1  \mcong{}  cd
11.  w1  \mneq{}  b
12.  w  :  Point
13.  c\_w\_d
14.  cw  \mcong{}  xy
15.  w  \mneq{}  d
16.  b'  :  Point
17.  a\_b'\_w1
18.  cw  \mcong{}  ab'
19.  wd  \mcong{}  b'w1
20.  a\_b'\_b
21.  ab'  \mcong{}  xy
\mvdash{}  b'  \mneq{}  b


By

---

Latex:
((Assert  b'\_w1\_b  BY  Auto)  THEN  Auto)

---

Home Index