let c be with_endpoints Curve of T; :: thesis: (T,c,c)

reconsider p = c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) as Path of the_first_point_of c, the_last_point_of c by Th29;

p,p are_homotopic by Th33, BORSUK_2:12;

hence (T,c,c) ; :: thesis: verum

reconsider p = c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) as Path of the_first_point_of c, the_last_point_of c by Th29;

p,p are_homotopic by Th33, BORSUK_2:12;

hence (T,c,c) ; :: thesis: verum