---

Step * of Lemma not-perp-point-construction

∀e:HeytingGeometry. ∀a,b,c:Point.
  (a # bc ⇒ (∃c',b':Point. ((c=c'=b' ∧ ab' ≅ ac) ∧ Colinear(a;b';b) ∧ a # c'b' ∧ Rac'b')))
BY
{ (Auto
   THEN (gProperProlong ⌜b⌝⌜a⌝`b\''⌜a⌝⌜c⌝⋅ THENA Auto)
   THEN (InstLemma `isosceles-mid-exists` [⌜e⌝;⌜c⌝;⌜a⌝;⌜b'⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜x⌝;⌜b'⌝]⋅
   THEN Auto) }

1
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'

2
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)
14. a # xb'
⊢ Raxb'

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.
    (a  \#  bc  {}\mRightarrow{}  (\mexists{}c',b':Point.  ((c=c'=b'  \mwedge{}  ab'  \00D0  ac)  \mwedge{}  Colinear(a;b';b)  \mwedge{}  a  \#  c'b'  \mwedge{}  Rac'b')))


By

---

Latex:
(Auto
  THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`b\mbackslash{}''\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `isosceles-mid-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index