:: deftheorem defines - XCMPLX_0:def 7 :
for x, y being Complex holds x - y = x + (- y);