---

Step * of Lemma use-plane-sep_strict

∀g:EuclideanPlane. ∀a,b,u,v:Point.  (u leftof ab ⇒ v leftof ba ⇒ (∃x:Point. (Colinear(a;b;x) ∧ u-x-v)))
BY
{ ((Auto THEN InstLemma `use-plane-sep` [⌜g⌝;⌜a⌝;⌜b⌝;⌜u⌝;⌜v⌝]⋅ THEN Auto)
   THEN ExRepD
   THEN InstConcl [⌜x⌝]⋅
   THEN Auto
   THEN (D 0 THEN Auto)
   THEN (InstLemma `lsep-iff-all-sep` [⌜g⌝;⌜u⌝;⌜b⌝;⌜a⌝]⋅ THENA Auto)) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. u : Point
5. v : Point
6. u leftof ab
7. v leftof ba
8. x : Point
9. Colinear(a;b;x)
10. u_x_v
11. Colinear(a;b;x)
12. u # ba ⇐⇒ (∀x:Point. (Colinear(x;b;a) ⇒ u ≠ x)) ∧ b ≠ a
⊢ u ≠ x

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. u : Point
5. v : Point
6. u leftof ab
7. v leftof ba
8. x : Point
9. Colinear(a;b;x)
10. u_x_v
11. Colinear(a;b;x)
12. u ≠ x
13. u # ba ⇐⇒ (∀x:Point. (Colinear(x;b;a) ⇒ u ≠ x)) ∧ b ≠ a
⊢ x ≠ v

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,u,v:Point.
    (u  leftof  ab  {}\mRightarrow{}  v  leftof  ba  {}\mRightarrow{}  (\mexists{}x:Point.  (Colinear(a;b;x)  \mwedge{}  u-x-v)))


By

---

Latex:
((Auto  THEN  InstLemma  `use-plane-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (D  0  THEN  Auto)
  THEN  (InstLemma  `lsep-iff-all-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index