---

Step * of Lemma ss-free-homotopic_weakening

No Annotations
∀X:SeparationSpace. ∀a,b:Point(X).  ss-free-homotopic(X;a;b) supposing a ≡ b
BY
{ (Auto THEN D 0 With ⌜λt.b⌝  THEN Auto THEN RepUR ``path-at`` 0 THEN Auto) }

1
.....wf..... 
1. X : SeparationSpace
2. a : Point(X)
3. b : Point(X)
4. a ≡ b
⊢ λt.b ∈ Point(Path(X))

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:SeparationSpace.  \mforall{}a,b:Point(X).    ss-free-homotopic(X;a;b)  supposing  a  \mequiv{}  b


By

---

Latex:
(Auto  THEN  D  0  With  \mkleeneopen{}\mlambda{}t.b\mkleeneclose{}    THEN  Auto  THEN  RepUR  ``path-at``  0  THEN  Auto)

---

Home Index