let a, b be Point of T; :: thesis: ( R62(T,a,b) implies R62(T,b,a) )
set P = the Path of a,b;
assume A1: a,b are_connected ; :: thesis: R62(T,b,a)
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, Th41; :: thesis: verum