let T be TopStruct ; 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; 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; ( t1,t2 are_connected implies p is Curve of T )
assume
t1,t2 are_connected
; 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
;
p is Curve of Tthen 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
;
verum end; end;