let T be non empty TopSpace; :: thesis: for a, b being Point of T st a,b are_connected holds
for A being Path of a,b holds A = - (- A)
let a, b be Point of T; :: thesis: ( a,b are_connected implies for A being Path of a,b holds A = - (- A) )
set I = the carrier of I[01];
assume A1: a,b are_connected ; :: thesis: for A being Path of a,b holds A = - (- A)
let A be Path of a,b; :: thesis: A = - (- A)
for x being Element of the carrier of I[01] holds A . x = (- (- A)) . x

proof

let x be Element of the carrier of I[01]; :: thesis: A . x = (- (- A)) . x
reconsider z = 1 - x as Point of I[01] by JORDAN5B:4;
thus (- (- A)) . x = (- A) . (1 - x) by A1, BORSUK_2:def 6
.= A . (1 - z) by A1, BORSUK_2:def 6
.= A . x ; :: thesis: verum

end;

hence A = - (- A) by FUNCT_2:63; :: thesis: verum