:: deftheorem defines / XXREAL_3:def 7 :
for x, y being ExtReal holds x / y = x * (y ");