:: deftheorem defines TrivDecomp BORSUK_1:def 6 :
for X being 1-sorted holds TrivDecomp X = Class (id the carrier of X);