let a, b be Point of [:S,T:]; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected
consider a1 being Point of S, a2 being Point of T such that
A1: a = [a1,a2] by BORSUK_1:10;
consider b1 being Point of S, b2 being Point of T such that
A2: b = [b1,b2] by BORSUK_1:10;
( a1,b1 are_connected & a2,b2 are_connected ) by BORSUK_2:def 3;
hence a,b are_connected by A1, A2, Th15; :: thesis: verum