let X be non empty pathwise_connected TopSpace; :: thesis: for a1, b1 being Point of X
for P, Q being Path of a1,b1 st P,Q are_homotopic holds
- P, - Q are_homotopic
let a1, b1 be Point of X; :: thesis: for P, Q being Path of a1,b1 st P,Q are_homotopic holds
- P, - Q are_homotopic
let P, Q be Path of a1,b1; :: thesis: ( P,Q are_homotopic implies - P, - Q are_homotopic )
a1,b1 are_connected by BORSUK_2:def 3;
hence ( P,Q are_homotopic implies - P, - Q are_homotopic ) by Th85; :: thesis: verum