---

Step * of Lemma lsep-opposite-iff

∀g:OrientedPlane. ∀a,b,x,y:Point.
  (x # ab ⇒ y # ab ⇒ (∃z:Point. (x_z_y ∧ Colinear(z;a;b)) ⇐⇒ x leftof ab ⇐⇒ y leftof ba))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN ExRepD
   THEN D 7
   THEN D 6
   THEN Auto
   THEN Try ((InstLemma  `not-left-and-right` [⌜g⌝;⌜x⌝;⌜a⌝;⌜b⌝]⋅ THEN Complete (Auto)))
   THEN Try ((InstLemma  `not-left-and-right` [⌜g⌝;⌜y⌝;⌜a⌝;⌜b⌝]⋅ THEN Complete (Auto)))) }

1
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ab
8. z : Point
9. x_z_y
10. Colinear(z;a;b)
11. x leftof ab
⊢ y leftof ba

2
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ba
7. y leftof ba
8. z : Point
9. x_z_y
10. Colinear(z;a;b)
11. y leftof ba
⊢ x leftof ab

3
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ba
7. y leftof ab
8. x leftof ab ⇒ y leftof ba
9. x leftof ab ⇐ y leftof ba
⊢ ∃z:Point. (x_z_y ∧ Colinear(z;a;b))

4
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ab
7. y leftof ba
8. x leftof ab ⇐ y leftof ba
9. y leftof ba
⊢ ∃z:Point. (x_z_y ∧ Colinear(z;a;b))

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}a,b,x,y:Point.
    (x  \#  ab  {}\mRightarrow{}  y  \#  ab  {}\mRightarrow{}  (\mexists{}z:Point.  (x\_z\_y  \mwedge{}  Colinear(z;a;b))  \mLeftarrow{}{}\mRightarrow{}  x  leftof  ab  \mLeftarrow{}{}\mRightarrow{}  y  leftof  ba))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ExRepD
  THEN  D  7
  THEN  D  6
  THEN  Auto
  THEN  Try  ((InstLemma    `not-left-and-right`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto)))
  THEN  Try  ((InstLemma    `not-left-and-right`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto))))

---

Home Index