---

Step * of Lemma left-between

No Annotations
∀g:OrientedPlane. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
BY
{ (Auto
   THEN (Assert ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z # ab) BY
               (D 1 THEN Unhide THEN Auto))
   ) }

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

2
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. x leftof ab
8. y leftof ab
9. B(xzy)
10. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z # ab)
⊢ z leftof ab

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:OrientedPlane.  \mforall{}a,b,x,y,z:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  B(xzy)  {}\mRightarrow{}  z  leftof  ab)


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}a,b,x,y,z:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  B(xzy)  {}\mRightarrow{}  z  \#  ab)  BY
                          (D  1  THEN  Unhide  THEN  Auto))
  )

---

Home Index