let T be non empty TopSpace; :: thesis: for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f is connected
let a, b be Point of T; :: thesis: for f being Path of a,b st a,b are_connected holds
rng f is connected
let f be Path of a,b; :: thesis: ( a,b are_connected implies rng f is connected )
assume A1: a,b are_connected ; :: thesis: rng f is connected
A2: dom f = the carrier of I[01] by FUNCT_2:def 1;
reconsider A = [.0 ,1.] as interval Subset of R^1 by TOPMETR:24;
reconsider B = A as Subset of I[01] by A2, BORSUK_1:83;
A3: B is connected by CONNSP_1:24;
A4: f is continuous by A1, BORSUK_2:def 2;
f .: B = rng f by A2, BORSUK_1:83, RELAT_1:146;
hence rng f is connected by A3, A4, TOPS_2:75; :: thesis: verum