:: deftheorem defines Pr1 BORSUK_1:def 4 :
for X, Y being non empty TopSpace holds Pr1 (X,Y) = .: (pr1 ( the carrier of X, the carrier of Y));