let n be 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 :: thesis: LSeg (p1,p2) c= rng g

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

proof

let y be object ; :: 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 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: verum

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: contradiction
hence contradiction by A1, A7, A6, A5, A4, Th2, XBOOLE_1:1; :: thesis: verum

end;

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