---

Step * 1 1 3 of Lemma geo-tar-opp-side-mid1


1. e : HeytingGeometry
2. a : Point
3. c : Point
4. r : Point
5. m : Point
6. a # rm
7. c # rm
8. t : Point
9. Colinear(r;m;t)
10. a_t_c
11. a=m=c
12. b : Point
13. r-a-b
14. b # rm
15. c # rm
16. x1 : Point
17. b-m-x1
18. mx1 ≅ bm
19. x : Point
20. r-m-x
21. mx ≅ rm
22. x_c_x1
⊢ x1-c-x
BY
{ (D 0 THEN Auto) }

1
1. e : HeytingGeometry
2. a : Point
3. c : Point
4. r : Point
5. m : Point
6. a # rm
7. c # rm
8. t : Point
9. Colinear(r;m;t)
10. a_t_c
11. a=m=c
12. b : Point
13. r-a-b
14. b # rm
15. c # rm
16. x1 : Point
17. b-m-x1
18. mx1 ≅ bm
19. x : Point
20. r-m-x
21. mx ≅ rm
22. x_c_x1
⊢ x1 ≠ c

2
1. e : HeytingGeometry
2. a : Point
3. c : Point
4. r : Point
5. m : Point
6. a # rm
7. c # rm
8. t : Point
9. Colinear(r;m;t)
10. a_t_c
11. a=m=c
12. b : Point
13. r-a-b
14. b # rm
15. c # rm
16. x1 : Point
17. b-m-x1
18. mx1 ≅ bm
19. x : Point
20. r-m-x
21. mx ≅ rm
22. x_c_x1
23. x1 ≠ c
⊢ c ≠ x

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  c  :  Point
4.  r  :  Point
5.  m  :  Point
6.  a  \#  rm
7.  c  \#  rm
8.  t  :  Point
9.  Colinear(r;m;t)
10.  a\_t\_c
11.  a=m=c
12.  b  :  Point
13.  r-a-b
14.  b  \#  rm
15.  c  \#  rm
16.  x1  :  Point
17.  b-m-x1
18.  mx1  \00D0  bm
19.  x  :  Point
20.  r-m-x
21.  mx  \00D0  rm
22.  x\_c\_x1
\mvdash{}  x1-c-x


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index