---

Step * of Lemma left-opposite-between

∀e:OrientedPlane. ∀a,b,p,q,x:Point.  (a_q_x ⇒ a leftof bp ⇒ q leftof pb ⇒ x leftof pb)
BY
{ (Auto
   THEN (FLemma `use-plane-sep` [-1;-2] THENA Auto)
   THEN ExRepD
   THEN RenameVar `z' (-3)
   THEN (Assert z_q_x BY
               Auto)
   THEN ThinVar `a') }

1
1. e : OrientedPlane
2. b : Point
3. p : Point
4. q : Point
5. x : Point
6. q leftof pb
7. z : Point
8. Colinear(p;b;z)
9. z_q_x
⊢ x leftof pb

---

Latex:

---

Latex:
\mforall{}e:OrientedPlane.  \mforall{}a,b,p,q,x:Point.    (a\_q\_x  {}\mRightarrow{}  a  leftof  bp  {}\mRightarrow{}  q  leftof  pb  {}\mRightarrow{}  x  leftof  pb)


By

---

Latex:
(Auto
  THEN  (FLemma  `use-plane-sep`  [-1;-2]  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `z'  (-3)
  THEN  (Assert  z\_q\_x  BY
                          Auto)
  THEN  ThinVar  `a')

---

Home Index