let T be non empty pathwise_connected TopSpace; :: thesis: for a, b being Point of T
for f being Path of a,b holds rng f = rng (- f)
let a, b be Point of T; :: thesis: for f being Path of a,b holds rng f = rng (- f)
let f be Path of a,b; :: thesis: rng f = rng (- f)
a,b are_connected by BORSUK_2:def 3;
hence rng f = rng (- f) by Th31; :: thesis: verum