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