let T be non empty TopSpace; 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; for f being Path of a,b st a,b are_connected holds
rng f = rng (- f)
let f be Path of a,b; ( a,b are_connected implies rng f = rng (- f) )
assume A1:
a,b are_connected
; rng f = rng (- f)
hence
rng f c= rng (- f)
by Lm7; XBOOLE_0:def 10 rng (- f) c= rng f
f = - (- f)
by A1, BORSUK_6:43;
hence
rng (- f) c= rng f
by A1, Lm7; verum