let T be non empty TopSpace; :: thesis: for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f = rng (- f)
let a, b be Point of T; :: thesis: for f being Path of a,b st a,b are_connected holds
rng f = rng (- f)
let f be Path of a,b; :: thesis: ( a,b are_connected implies rng f = rng (- f) )
assume A1: a,b are_connected ; :: thesis: rng f = rng (- f)
hence rng f c= rng (- f) by Lm7; :: according to XBOOLE_0:def 10 :: thesis: rng (- f) c= rng f
f = - (- f) by A1, BORSUK_6:43;
hence rng (- f) c= rng f by A1, Lm7; :: thesis: verum