---

Step * of Lemma geo-SCS_wf

∀[g:EuclideanPlane]
  ∀c,d,a:Point. ∀b:{b:Point| b ≠ a ∧ c_b_d} .
    (SCS(a;b;c;d) ∈ {v:Point| cv ≅ cd ∧ (v_b_SCO(a;b;c;d) ∧ Colinear(a;b;v)) ∧ (b ≠ d ⇒ v ≠ SCO(a;b;c;d))} )
BY
{ (Auto
   THEN Unfolds ``geo-SCS geo-SCO`` 0
   THEN (GenConclTerm ⌜SC(a;b;c;d)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN DSetVars
   THEN (GenConclTerm ⌜SymmetricPoint(v;a)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `a\'' (-1)
   THEN RepeatFor 2 (D -1)
   THEN (Assert b_v_a' BY
               Auto)) }

1
1. g : EuclideanPlane
2. c : Point
3. d : Point
4. a : Point
5. b : Point
6. b ≠ a ∧ c_b_d
7. v : Point
8. cv ≅ cd ∧ a_b_v ∧ (b ≠ d ⇒ b ≠ v)
9. a' : Point
10. a_v_a'
11. av ≅ va'
12. b_v_a'
⊢ SC(a';b;c;d) ∈ {v@0:Point| cv@0 ≅ cd ∧ (v@0_b_v ∧ Colinear(a;b;v@0)) ∧ (b ≠ d ⇒ v@0 ≠ v)} 

---

Latex:

---

Latex:
\mforall{}[g:EuclideanPlane]
    \mforall{}c,d,a:Point.  \mforall{}b:\{b:Point|  b  \mneq{}  a  \mwedge{}  c\_b\_d\}  .
        (SCS(a;b;c;d)  \mmember{}  \{v:Point| 
                                          cv  \mcong{}  cd  \mwedge{}  (v\_b\_SCO(a;b;c;d)  \mwedge{}  Colinear(a;b;v))  \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  v  \mneq{}  SCO(a;b;c;d))\}  )


By

---

Latex:
(Auto
  THEN  Unfolds  ``geo-SCS  geo-SCO``  0
  THEN  (GenConclTerm  \mkleeneopen{}SC(a;b;c;d)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  DSetVars
  THEN  (GenConclTerm  \mkleeneopen{}SymmetricPoint(v;a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `a\mbackslash{}''  (-1)
  THEN  RepeatFor  2  (D  -1)
  THEN  (Assert  b\_v\_a'  BY
                          Auto))

---

Home Index