let T be non empty TopSpace; :: thesis: for a being Point of T
for P, Q being constant Path of a,a holds P,Q are_homotopic
let a be Point of T; :: thesis: for P, Q being constant Path of a,a holds P,Q are_homotopic
let P, Q be constant Path of a,a; :: thesis: P,Q are_homotopic
( P = I[01] --> a & Q = I[01] --> a ) by BORSUK_2:5;
hence P,Q are_homotopic by BORSUK_2:12; :: thesis: verum