:: deftheorem defines is_an_SDR_of BORSUK_1:def 18 :
for X being non empty TopSpace
for Y being non empty SubSpace of X holds
( Y is_an_SDR_of X iff ex H being continuous Function of [:X,I[01]:],X st
for A being Point of X holds
( H . [A,0[01]] = A & H . [A,1[01]] in the carrier of Y & ( A in the carrier of Y implies for T being Point of I[01] holds H . [A,T] = A ) ) );