---

Step * 1 of Lemma right-angle-colinear2


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. c' : Point
6. Rabc
7. c ≠ b
8. Colinear(b;c;c')
9. a ≠ b
⊢ Rabc'
BY
{ ((FLemma `right-angle-symmetry` [6] THEN Auto)
   THEN InstLemma `right-angle-colinear` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜c'⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  c'  :  Point
6.  Rabc
7.  c  \mneq{}  b
8.  Colinear(b;c;c')
9.  a  \mneq{}  b
\mvdash{}  Rabc'


By

---

Latex:
((FLemma  `right-angle-symmetry`  [6]  THEN  Auto)
  THEN  InstLemma  `right-angle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index