---

Step * of Lemma left-transitivity

No Annotations
∀g:OrientedPlane. ∀a,b,x,y,z:Point.
  (x leftof ab ⇒ y leftof ab ⇒ z leftof ab ⇒ y leftof ax ⇒ z leftof ay ⇒ (¬z leftof xa))
BY
{ (Auto THEN (D 0 THENA Auto⋅) THEN (FLemma `use-plane-sep` [-1;-3] THENA Auto) THEN ExRepD THEN RenameVar `w' (-3)) }

1
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. z leftof ab
10. y leftof ax
11. z leftof ay
12. z leftof xa
13. w : Point
14. Colinear(x;a;w)
15. B(zwy)
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:OrientedPlane.  \mforall{}a,b,x,y,z:Point.
    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  z  leftof  ab  {}\mRightarrow{}  y  leftof  ax  {}\mRightarrow{}  z  leftof  ay  {}\mRightarrow{}  (\mneg{}z  leftof  xa))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto\mcdot{})
  THEN  (FLemma  `use-plane-sep`  [-1;-3]  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `w'  (-3))

---

Home Index