let T be non empty TopSpace; :: thesis: for a, b being Point of T
for P being Path of a,b st P is continuous & P . 0 = a & P . 1 = b holds
( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )
let a, b be Point of T; :: thesis: for P being Path of a,b st P is continuous & P . 0 = a & P . 1 = b holds
( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )
let P be Path of a,b; :: thesis: ( P is continuous & P . 0 = a & P . 1 = b implies ( - P is continuous & (- P) . 0 = b & (- P) . 1 = a ) )
assume that
A1: P is continuous and
A2: ( P . 0 = a & P . 1 = b ) ; :: thesis: ( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )
A3: (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a by A2, Th40;
( P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b ) by A1, A2, Th39, Th40;
then b,a are_connected by A3;
hence ( - P is continuous & (- P) . 0 = b & (- P) . 1 = a ) by BORSUK_2:def 2; :: thesis: verum