let T be non empty TopSpace; :: thesis: for t being Point of T
for C1, C2 being constant Loop of t holds C1,C2 are_homotopic
let t be Point of T; :: thesis: for C1, C2 being constant Loop of t holds C1,C2 are_homotopic
let C1, C2 be constant Loop of t; :: thesis: C1,C2 are_homotopic
C1 = I[01] --> t by BORSUK_2:5
.= C2 by BORSUK_2:5 ;
hence C1,C2 are_homotopic by BORSUK_2:12; :: thesis: verum