let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T holds dom c = [.(inf (dom c)),(sup (dom c)).]
let c be with_endpoints Curve of T; :: thesis: dom c = [.(inf (dom c)),(sup (dom c)).]
reconsider f = c as parametrized-curve PartFunc of R^1,T by Th23;
dom f is interval Subset of REAL by Def4;
then reconsider A = dom c as ext-real-membered left_end right_end interval set by Def6, Def7;
A = [.(min A),(max A).] by XXREAL_2:75;
hence dom c = [.(inf (dom c)),(sup (dom c)).] ; :: thesis: verum