---

Step * of Lemma path-comp-rel_wf

No Annotations
∀[X:SeparationSpace]. ∀[f,g,h:Point(Path(X))].  (path-comp-rel(X;f;g;h) ∈ ℙ)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto) }

1
1. X : SeparationSpace
2. f : Point(Path(X))
3. g : Point(Path(X))
4. h : Point(Path(X))
5. ∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . h@t ≡ f@r(2) * t
6. ∀x:ℝ. (((r1/r(2)) ≤ x) ∧ (x ≤ r1) ∈ Type)
7. t : ℝ@i
8. r1 ≤ (r(2) * t)
9. t ≤ r1
10. r0 ≤ ((r(2) * t) - r1)
⊢ ((r(2) * t) - r1) ≤ r1

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:SeparationSpace].  \mforall{}[f,g,h:Point(Path(X))].    (path-comp-rel(X;f;g;h)  \mmember{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Auto)

---

Home Index