---

Step * 1 of Lemma not-perp-point-construction


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. b' : Point
7. b-a-b'
8. ab' ≅ ac
9. x : Point
10. c=x=b'
11. c=x=b'
12. ab' ≅ ac
13. Colinear(a;b';b)
⊢ a # xb'
BY
{ ((InstLemma `geo-triangle-colinear` [⌜e⌝;⌜c⌝;⌜b'⌝;⌜a⌝;⌜x⌝]⋅ THEN Auto)
   THENA ((D 11 THEN InstLemma  `midpoint-sep` [⌜e⌝;⌜c⌝;⌜b'⌝;⌜x⌝]⋅)
          THEN InstLemma `geo-triangle-colinear` [⌜e⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜b'⌝]⋅
          THEN Auto)
   ) }

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  b'  :  Point
7.  b-a-b'
8.  ab'  \00D0  ac
9.  x  :  Point
10.  c=x=b'
11.  c=x=b'
12.  ab'  \00D0  ac
13.  Colinear(a;b';b)
\mvdash{}  a  \#  xb'


By

---

Latex:
((InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THENA  ((D  11  THEN  InstLemma    `midpoint-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{})
                THEN  InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}
                THEN  Auto)
  )

---

Home Index