let f, g be ext-real number ; :: thesis: - (f + g) = (- f) - g
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def 1;
hence - (f + g) = (- f) - g by EXTREAL2:14; :: thesis: verum