---

Step * 1 1 of Lemma geo-out-triangle


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. b # ac
8. out(b aa')
9. out(b cc')
10. out(b aa') ⇐ (Colinear(b;a;a') ∧ (¬a_b_a')) ∧ b ≠ a ∧ b ≠ a'
11. Colinear(b;a;a')
12. ¬a_b_a'
13. b ≠ a
14. b ≠ a'
15. out(b cc') ⇐ (Colinear(b;c;c') ∧ (¬c_b_c')) ∧ b ≠ c ∧ b ≠ c'
16. Colinear(b;c;c')
17. ¬c_b_c'
18. b ≠ c
19. b ≠ c'
⊢ b # a'c'
BY
{ ((InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a'⌝]⋅ THENA Auto)
   THEN InstLemma `geo-triangle-colinear` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a'⌝;⌜c'⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  c'  :  Point
7.  b  \#  ac
8.  out(b  aa')
9.  out(b  cc')
10.  out(b  aa')  \mLeftarrow{}{}  (Colinear(b;a;a')  \mwedge{}  (\mneg{}a\_b\_a'))  \mwedge{}  b  \mneq{}  a  \mwedge{}  b  \mneq{}  a'
11.  Colinear(b;a;a')
12.  \mneg{}a\_b\_a'
13.  b  \mneq{}  a
14.  b  \mneq{}  a'
15.  out(b  cc')  \mLeftarrow{}{}  (Colinear(b;c;c')  \mwedge{}  (\mneg{}c\_b\_c'))  \mwedge{}  b  \mneq{}  c  \mwedge{}  b  \mneq{}  c'
16.  Colinear(b;c;c')
17.  \mneg{}c\_b\_c'
18.  b  \mneq{}  c
19.  b  \mneq{}  c'
\mvdash{}  b  \#  a'c'


By

---

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

---

Home Index