---

Step * 2 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)
14. a # xb'
⊢ Raxb'
BY
{ ((Unfold `right-angle` 0 THEN Auto)
   THEN InstLemma `symmetric-point-unicity` [⌜e⌝;⌜x⌝;⌜b'⌝;⌜c'⌝;⌜c⌝]⋅
   THEN EAuto 1
   THEN EliminatePoint (-1)
   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)
14.  a  \#  xb'
\mvdash{}  Raxb'


By

---

Latex:
((Unfold  `right-angle`  0  THEN  Auto)
  THEN  InstLemma  `symmetric-point-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1
  THEN  EliminatePoint  (-1)
  THEN  Auto)

---

Home Index