---

Step * 1 of Lemma geo-triangle-separation


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. c # ba
7. c # ab
8. a ≠ c
9. ¬a_b_c
10. ∀z:Point. (z ≠ b ⇒ Colinear(a;b;z) ⇒ z # bc)
11. x : Point
12. y : Point
13. (Colinear(a;b;x) ∧ Colinear(c;b;y)) ∧ x ≠ b ∧ y ≠ b
⊢ x # by ∧ (∀m:Point. (x-m-y ⇒ m ≠ b))
BY
{ ((Assert x # bc BY
          Auto)
   THEN (Assert c # bx BY
               (FLemma `geo-triangle-implies` [-1] THEN Auto))
   THEN (FLemma `geo-triangle-implies` [-1] THENA Auto)
   THEN SplitAndHyps) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. c # ba
7. c # ab
8. a ≠ c
9. ¬a_b_c
10. ∀z:Point. (z ≠ b ⇒ Colinear(a;b;z) ⇒ z # bc)
11. x : Point
12. y : Point
13. Colinear(a;b;x)
14. Colinear(c;b;y)
15. x ≠ b
16. y ≠ b
17. x # bc
18. c # bx
19. x # bc
20. x # cb
21. c ≠ x
22. ¬c_b_x
23. ∀z:Point. (z ≠ b ⇒ Colinear(c;b;z) ⇒ z # bx)
⊢ x # by ∧ (∀m:Point. (x-m-y ⇒ m ≠ b))

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  c  \#  ba
7.  c  \#  ab
8.  a  \mneq{}  c
9.  \mneg{}a\_b\_c
10.  \mforall{}z:Point.  (z  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;z)  {}\mRightarrow{}  z  \#  bc)
11.  x  :  Point
12.  y  :  Point
13.  (Colinear(a;b;x)  \mwedge{}  Colinear(c;b;y))  \mwedge{}  x  \mneq{}  b  \mwedge{}  y  \mneq{}  b
\mvdash{}  x  \#  by  \mwedge{}  (\mforall{}m:Point.  (x-m-y  {}\mRightarrow{}  m  \mneq{}  b))


By

---

Latex:
((Assert  x  \#  bc  BY
                Auto)
  THEN  (Assert  c  \#  bx  BY
                          (FLemma  `geo-triangle-implies`  [-1]  THEN  Auto))
  THEN  (FLemma  `geo-triangle-implies`  [-1]  THENA  Auto)
  THEN  SplitAndHyps)

---

Home Index