let T be TopStruct ; :: thesis: for t1, t2 being Point of T
for p being Path of t1,t2 st t1,t2 are_connected holds
p is Curve of T
let t1, t2 be Point of T; :: thesis: for p being Path of t1,t2 st t1,t2 are_connected holds
p is Curve of T
let p be Path of t1,t2; :: thesis: ( t1,t2 are_connected implies p is Curve of T )
assume t1,t2 are_connected ; :: thesis: p is Curve of T
then A1: ( p is continuous & p . 0 = t1 & p . 1 = t2 ) by BORSUK_2:def 2;

per cases ( not T is empty or T is empty ) ;

suppose not T is empty ; :: thesis: p is Curve of T

then A2: [#] I[01] = dom p by FUNCT_2:def 1;
then A3: dom p c= [#] R^1 by PRE_TOPC:def 4;
then reconsider A = dom p as Subset of R^1 ;
A4: I[01] = R^1 | A by A2, BORSUK_1:40, TOPMETR:19, TOPMETR:20;
rng p c= [#] T ;
then reconsider c = p as PartFunc of R^1,T by A3, RELSET_1:4;
reconsider c = c as parametrized-curve PartFunc of R^1,T by A2, A4, Def4, A1, BORSUK_1:40;
c is Element of Curves T by Th20;
hence p is Curve of T ; :: thesis: verum

end;

suppose A5: T is empty ; :: thesis: p is Curve of T

then reconsider c = p as PartFunc of R^1,T ;
c = {} by A5;
then reconsider c = c as parametrized-curve PartFunc of R^1,T by Lm1;
c is Element of Curves T by Th20;
hence p is Curve of T ; :: thesis: verum

end;

end;