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 and
A3: P . 1 = b ; :: thesis: ( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )
( P * (L[01] (0 ,1 (#) ),((#) 0 ,1)) is continuous Function of I[01] ,T & (P * (L[01] (0 ,1 (#) ),((#) 0 ,1))) . 0 = b & (P * (L[01] (0 ,1 (#) ),((#) 0 ,1))) . 1 = a ) by A1, A2, A3, Th43, Th44;
then b,a are_connected by BORSUK_2:def 1;
hence ( - P is continuous & (- P) . 0 = b & (- P) . 1 = a ) by BORSUK_2:def 2; :: thesis: verum