---

Step * 1 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. (Colinear(r;m;t) ∧ a_t_c)
9. a=m=c
10. b : Point
11. r-a-b
12. b # rm
13. c # rm
⊢ ∃t:Point. (Colinear(r;m;t) ∧ b_t_c)
BY
{ (((InstLemma `geo-proper-extend-exists` [⌜e⌝;⌜b⌝;⌜m⌝;⌜b⌝;⌜m⌝]⋅ THENA Auto)
    THEN (InstLemma `geo-proper-extend-exists` [⌜e⌝;⌜r⌝;⌜m⌝;⌜r⌝;⌜m⌝]⋅ THENA Auto)
    )
   THEN ExRepD
   ) }

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
⊢ ∃t:Point. (Colinear(r;m;t) ∧ b_t_c)

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  c  :  Point
4.  r  :  Point
5.  m  :  Point
6.  a  \#  rm
7.  c  \#  rm
8.  \mexists{}t:Point.  (Colinear(r;m;t)  \mwedge{}  a\_t\_c)
9.  a=m=c
10.  b  :  Point
11.  r-a-b
12.  b  \#  rm
13.  c  \#  rm
\mvdash{}  \mexists{}t:Point.  (Colinear(r;m;t)  \mwedge{}  b\_t\_c)


By

---

Latex:
(((InstLemma  `geo-proper-extend-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (InstLemma  `geo-proper-extend-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
    )
  THEN  ExRepD
  )

---

Home Index