let n be Nat; :: thesis:
let p1, p2 be Point of (TOP-REAL n); :: thesis:
let g be Path of p1,p2; :: thesis:
assume A1: rng g c= LSeg (p1,p2) ; :: thesis:
A2: p2 = g . 1 by BORSUK_2:def 4;
A3: p1 = g . 0 by BORSUK_2:def 4;

now :: thesis:

A4: g .: ([#] I[01]) c= rng g

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in g .: ([#] I[01]) ; :: thesis:
then ex x being object st
( x in dom g & x in [#] I[01] & y = g . x ) by FUNCT_1:def 6;
hence y in rng g by FUNCT_1:def 3; :: thesis:

end;

1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom g by FUNCT_2:def 1;
then A5: p2 in g .: ([#] I[01]) by A2, FUNCT_1:def 6;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def 1;
then A6: p1 in g .: ([#] I[01]) by A3, FUNCT_1:def 6;
[#] I[01] is connected by CONNSP_1:27;
then A7: g .: ([#] I[01]) is connected by TOPS_2:61;
assume not LSeg (p1,p2) c= rng g ; :: thesis:
hence contradiction by A1, A7, A6, A5, A4, Th2, XBOOLE_1:1; :: thesis:

end;

hence rng g = LSeg (p1,p2) by A1; :: thesis: