set t = the Point of T;
set f = I[01] --> the Point of T;
A1: ( (I[01] --> the Point of T) . 0 = the Point of T & (I[01] --> the Point of T) . 1 = the Point of T ) by BORSUK_1:def 14, BORSUK_1:def 15;
set p = the Path of the Point of T, the Point of T;
the Point of T, the Point of T are_connected by A1;
then reconsider c = the Path of the Point of T, the Point of T as Curve of T by Th22;
take c ; :: thesis: c is with_endpoints
A2: dom c = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
set S = [.0,1.];
inf [.0,1.] = 0 by XXREAL_2:25;
then inf [.0,1.] in [.0,1.] by XXREAL_1:1;
hence dom c is left_end by A2, XXREAL_2:def 5; :: according to TOPALG_6:def 6,TOPALG_6:def 8 :: thesis: c is with_last_point
sup [.0,1.] = 1 by XXREAL_2:29;
then sup [.0,1.] in [.0,1.] by XXREAL_1:1;
hence dom c is right_end by A2, XXREAL_2:def 6; :: according to TOPALG_6:def 7 :: thesis: verum