:: deftheorem defines --> CC0SP2:def 2 :
for X being 1-sorted
for y being Complex holds X --> y = the carrier of X --> y;