theorem :: XXREAL_3:63

for x, y, t being ExtReal st t <> -infty & t <> +infty & x < y holds
x - t < y - t