a,b are_connected by Def3;
hence for P being Path of a,b holds P,P are_homotopic by Th15; :: thesis: verum