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

now

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

proof

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

end;

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

end;

hence rng g = LSeg p1,p2 by A1, XBOOLE_0:def 10; :: thesis: verum