---

Step * of Lemma left-convex

No Annotations
∀g:EuclideanPlane. ∀a,b,x,y:Point.  (x leftof ab ⇒ (B(bxy) ∨ (B(byx) ∧ y # b)) ⇒ y leftof ab)
BY
{ (Auto THEN D -1) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. B(bxy)
⊢ y leftof ab

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. B(byx) ∧ y # b
⊢ y leftof ab

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  \mforall{}a,b,x,y:Point.    (x  leftof  ab  {}\mRightarrow{}  (B(bxy)  \mvee{}  (B(byx)  \mwedge{}  y  \#  b))  {}\mRightarrow{}  y  leftof  ab)


By

---

Latex:
(Auto  THEN  D  -1)

---

Home Index