---

Step * of Lemma geo-CC_functionality

∀[g:EuclideanPlane]. ∀[a,b:Point]. ∀[c:{c:Point| a ≠ c} ]. ∀[d:{d:Point| StrictOverlap(a;b;c;d)} ]. ∀[a',b':Point].
∀[c':{c':Point| a' ≠ c'} ]. ∀[d':{d':Point| StrictOverlap(a';b';c';d')} ].
  (CC(a;b;c;d) ≡ CC(a';b';c';d')) supposing (d ≡ d' and c ≡ c' and b ≡ b' and a ≡ a')
BY
{ (Auto THEN GenConclTerms Auto [CC(a;b;c;d);⌜CC(a';b';c';d')⌝]⋅) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : {c:Point| a ≠ c} 
5. d : {d:Point| StrictOverlap(a;b;c;d)} 
6. a' : Point
7. b' : Point
8. c' : {c':Point| a' ≠ c'} 
9. d' : {d':Point| StrictOverlap(a';b';c';d')} 
10. a ≡ a'
11. b ≡ b'
12. c ≡ c'
13. d ≡ d'
14. v : {u:Point| ab ≅ au ∧ cd ≅ cu ∧ u leftof ac} 
15. CC(a;b;c;d) = v ∈ {u:Point| ab ≅ au ∧ cd ≅ cu ∧ u leftof ac} 
16. v1 : {u:Point| a'b' ≅ a'u ∧ c'd' ≅ c'u ∧ u leftof a'c'} 
17. CC(a';b';c';d') = v1 ∈ {u:Point| a'b' ≅ a'u ∧ c'd' ≅ c'u ∧ u leftof a'c'} 
⊢ v ≡ v1

---

Latex:

---

Latex:
\mforall{}[g:EuclideanPlane].  \mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  a  \mneq{}  c\}  ].  \mforall{}[d:\{d:Point|  StrictOverlap(a;b;c;d)\}  ].
\mforall{}[a',b':Point].  \mforall{}[c':\{c':Point|  a'  \mneq{}  c'\}  ].  \mforall{}[d':\{d':Point|  StrictOverlap(a';b';c';d')\}  ].
    (CC(a;b;c;d)  \mequiv{}  CC(a';b';c';d'))  supposing  (d  \mequiv{}  d'  and  c  \mequiv{}  c'  and  b  \mequiv{}  b'  and  a  \mequiv{}  a')


By

---

Latex:
(Auto  THEN  GenConclTerms  Auto  [CC(a;b;c;d);\mkleeneopen{}CC(a';b';c';d')\mkleeneclose{}]\mcdot{})

---

Home Index