---

Step * 1 2 of Lemma sq_stable__geo-left-1


1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. ∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
4. a : Point
5. b : Point
6. c : Point
7. ∀a:Point. a ≡ a
8. ∀a,b:Point.  ab ≅ ba
9. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
10. a leftof bc
11. a # bc
12. a leftof cb
13. x : Point
14. Colinear(b;c;x)
15. B(axa)
16. a ≡ x
⊢ False
BY
{ ((D 2 THEN SplitAndHyps)
   THEN (InstHyp [⌜b⌝;⌜c⌝;⌜a⌝;⌜a⌝;⌜x⌝] (13)⋅ THENA Auto)
   THEN (D 26 THENA Auto)
   THEN Unfold `geo-lsep` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlaneStructure
2.  BasicGeometryAxioms(g)
3.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mneg{}Colinear(a;b;c)))
4.  a  :  Point
5.  b  :  Point
6.  c  :  Point
7.  \mforall{}a:Point.  a  \mequiv{}  a
8.  \mforall{}a,b:Point.    ab  \mcong{}  ba
9.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
10.  a  leftof  bc
11.  a  \#  bc
12.  a  leftof  cb
13.  x  :  Point
14.  Colinear(b;c;x)
15.  B(axa)
16.  a  \mequiv{}  x
\mvdash{}  False


By

---

Latex:
((D  2  THEN  SplitAndHyps)
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (13)\mcdot{}  THENA  Auto)
  THEN  (D  26  THENA  Auto)
  THEN  Unfold  `geo-lsep`  0
  THEN  Auto)

---

Home Index