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