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

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