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: ( p1 = g . 0 & p2 = g . 1 ) by BORSUK_2:def 4;

now

assume A3: not LSeg p1,p2 c= rng g ; :: thesis: contradiction
[#] I[01] is connected by CONNSP_1:28;
then A4: g .: ([#] I[01] ) is connected by TOPS_2:75;
0 in the carrier of I[01] by BORSUK_1:86;
then 0 in dom g by FUNCT_2:def 1;
then A5: p1 in g .: ([#] I[01] ) by A2, FUNCT_1:def 12;
1 in the carrier of I[01] by BORSUK_1:86;
then 1 in dom g by FUNCT_2:def 1;
then A6: p2 in g .: ([#] I[01] ) by A2, FUNCT_1:def 12;
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;

hence contradiction by A1, A3, A4, A5, A6, Th2, XBOOLE_1:1; :: thesis: verum

end;

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