let X be non empty pathwise_connected TopSpace; :: thesis: for a1, b1 being Point of X
for P being Path of a1,b1
for Q being constant Path of b1,b1 holds P + Q,P are_homotopic
let a1, b1 be Point of X; :: thesis: for P being Path of a1,b1
for Q being constant Path of b1,b1 holds P + Q,P are_homotopic
let P be Path of a1,b1; :: thesis: for Q being constant Path of b1,b1 holds P + Q,P are_homotopic
let Q be constant Path of b1,b1; :: thesis: P + Q,P are_homotopic
a1,b1 are_connected by BORSUK_2:def 3;
hence P + Q,P are_homotopic by Th88; :: thesis: verum