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