---

Step * 1 1 of Lemma sq_stable__geo-left-1

.....assertion..... 
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)
⊢ a ≡ x
BY
{ ((D 0 THENA Auto) THEN Unfold `geo-between` 15 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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)
\mvdash{}  a  \mequiv{}  x


By

---

Latex:
((D  0  THENA  Auto)  THEN  Unfold  `geo-between`  15  THEN  Auto)

---

Home Index