---

Step * 1 of Lemma left-between

.....aux..... 
1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. a : Point
4. b : Point
5. x : Point
6. y : Point
7. z : Point
8. x leftof ab
9. y leftof ab
10. B(xzy)
11. a1 : Point
12. b1 : Point
13. x1 : Point
14. y1 : Point
15. z1 : Point
16. x1 leftof a1b1
17. y1 leftof a1b1
18. B(x1z1y1)
⊢ z1 # a1b1
BY
{ ((D 2 THEN ExRepD) THEN (FHyp (13) [28;29;30] THENA Auto) THEN Unfold `geo-lsep` 0 THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  g  :  EuclideanPlaneStructure
2.  BasicGeometryAxioms(g)
3.  a  :  Point
4.  b  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  x  leftof  ab
9.  y  leftof  ab
10.  B(xzy)
11.  a1  :  Point
12.  b1  :  Point
13.  x1  :  Point
14.  y1  :  Point
15.  z1  :  Point
16.  x1  leftof  a1b1
17.  y1  leftof  a1b1
18.  B(x1z1y1)
\mvdash{}  z1  \#  a1b1


By

---

Latex:
((D  2  THEN  ExRepD)  THEN  (FHyp  (13)  [28;29;30]  THENA  Auto)  THEN  Unfold  `geo-lsep`  0  THEN  Auto)

---

Home Index