---

Step * 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')
⊢ b # a'c'
BY
{ (((((InstLemma `geo-out-iff-colinear` [⌜e⌝;⌜b⌝;⌜a⌝;⌜a'⌝]⋅ THENA Auto) THEN D -1) THEN (D -2 THENA EAuto 1))
    THEN ((InstLemma `geo-out-iff-colinear` [⌜e⌝;⌜b⌝;⌜c⌝;⌜c'⌝]⋅ THENA Auto) THEN D -1)
    THEN (D -2 THENA EAuto 1))
   THEN ExRepD
   ) }

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

---

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')
\mvdash{}  b  \#  a'c'


By

---

Latex:
(((((InstLemma  `geo-out-iff-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)
      THEN  (D  -2  THENA  EAuto  1)
      )
    THEN  ((InstLemma  `geo-out-iff-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)
    THEN  (D  -2  THENA  EAuto  1))
  THEN  ExRepD
  )

---

Home Index