let a, b be Point of T; :: thesis: ( a,b are_connected implies b,a are_connected )
consider P being Path of a,b;
assume A1: a,b are_connected ; :: thesis: b,a are_connected
then A2: P . 1 = b by BORSUK_2:def 2;
take - P ; :: according to BORSUK_2:def 1 :: thesis: ( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )
( P is continuous & P . 0 = a ) by A1, BORSUK_2:def 2;
hence ( - P is continuous & (- P) . 0 = b & (- P) . 1 = a ) by A2, Th45; :: thesis: verum