:: deftheorem defines - XXREAL_3:def 4 :
for x, y being ExtReal holds x - y = x + (- y);