:: deftheorem defines Pr2 BORSUK_1:def 5 :
for X, Y being non empty TopSpace holds Pr2 (X,Y) = .: (pr2 ( the carrier of X, the carrier of Y));