let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T holds
( the_first_point_of c in rng c & the_last_point_of c in rng c )
let c be with_endpoints Curve of T; :: thesis: ( the_first_point_of c in rng c & the_last_point_of c in rng c )
A1: inf (dom c) <= sup (dom c) by XXREAL_2:40;
dom c = [.(inf (dom c)),(sup (dom c)).] by Th27;
then ( inf (dom c) in dom c & sup (dom c) in dom c ) by A1, XXREAL_1:1;
hence ( the_first_point_of c in rng c & the_last_point_of c in rng c ) by FUNCT_1:3; :: thesis: verum