let a, b be Point of [:S,T:]; BORSUK_2:def 3 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; verum