---

Step * of Lemma geo-SS_functionality

∀[g:EuclideanPlane]. ∀[a,b:Point]. ∀[u:{u:Point| u leftof ab} ]. ∀[v:{v:Point| v leftof ba} ]. ∀[a',b':Point].
∀[u':{u:Point| u leftof a'b'} ]. ∀[v':{v:Point| v leftof b'a'} ].
  (geo-SS(g;a;b;u;v) ≡ geo-SS(g;a';b';u';v')) supposing (v ≡ v' and u ≡ u' and b ≡ b' and a ≡ a')
BY
{ (Auto
   THEN GenConclTerms Auto [geo-SS(g;a;b;u;v);⌜geo-SS(g;a';b';u';v')⌝]⋅
   THEN Thin (-1)
   THEN Thin (-2)
   THEN D -2
   THEN D -1
   THEN Unhide
   THEN Auto) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. u : {u:Point| u leftof ab} 
5. v : {v:Point| v leftof ba} 
6. a' : Point
7. b' : Point
8. u' : {u:Point| u leftof a'b'} 
9. v' : {v:Point| v leftof b'a'} 
10. a ≡ a'
11. b ≡ b'
12. u ≡ u'
13. v ≡ v'
14. v1 : Point
15. Colinear(a;b;v1)
16. B(uv1v)
17. v2 : Point
18. Colinear(a';b';v2)
19. B(u'v2v')
⊢ v1 ≡ v2

---

Latex:

---

Latex:
\mforall{}[g:EuclideanPlane].  \mforall{}[a,b:Point].  \mforall{}[u:\{u:Point|  u  leftof  ab\}  ].  \mforall{}[v:\{v:Point|  v  leftof  ba\}  ].
\mforall{}[a',b':Point].  \mforall{}[u':\{u:Point|  u  leftof  a'b'\}  ].  \mforall{}[v':\{v:Point|  v  leftof  b'a'\}  ].
    (geo-SS(g;a;b;u;v)  \mequiv{}  geo-SS(g;a';b';u';v'))  supposing  (v  \mequiv{}  v'  and  u  \mequiv{}  u'  and  b  \mequiv{}  b'  and  a  \mequiv{}  a')


By

---

Latex:
(Auto
  THEN  GenConclTerms  Auto  [geo-SS(g;a;b;u;v);\mkleeneopen{}geo-SS(g;a';b';u';v')\mkleeneclose{}]\mcdot{}
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  D  -2
  THEN  D  -1
  THEN  Unhide
  THEN  Auto)

---

Home Index