---

Step * of Lemma geo-SCS-out

∀e:EuclideanPlane. ∀a:Point. ∀x,b:{b:Point| a ≠ b} .  out(a bSCS(b;a;a;x))
BY
{ (Auto
   THEN GenConclTerm ⌜SCS(b;a;a;x)⌝⋅
   THEN Auto
   THEN DSetVars
   THEN Unhide
   THEN Auto
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. x : Point
4. a ≠ x
5. b : Point
6. a ≠ b
7. v : Point
8. av ≅ ax
9. v_a_SCO(b;a;a;x)
10. Colinear(b;a;v)
11. SCS(b;a;a;x) = v ∈ {v:Point| av ≅ ax ∧ (v_a_SCO(b;a;a;x) ∧ Colinear(b;a;v)) ∧ (a ≠ x ⇒ v ≠ SCO(b;a;a;x))} 
12. v ≠ SCO(b;a;a;x)
13. a ≠ v
14. ¬a_b_v
15. ¬a_v_b
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}x,b:\{b:Point|  a  \mneq{}  b\}  .    out(a  bSCS(b;a;a;x))


By

---

Latex:
(Auto
  THEN  GenConclTerm  \mkleeneopen{}SCS(b;a;a;x)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  DSetVars
  THEN  Unhide
  THEN  Auto
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index