let x, y, t be ExtReal; :: thesis: ( t <> -infty & t <> +infty & x < y implies x - t < y - t )
assume that
A1: ( t <> -infty & t <> +infty ) and
A2: x < y ; :: thesis: x - t < y - t
A3: t - t = 0 by Th7;
A4: now :: thesis: not x - t = y - t
assume x - t = y - t ; :: thesis: contradiction
then x - (t - t) = (y - t) + t by A1, Th32;
then x - 0 = y - (t - t) by A1, A3, Th32;
then x = y + 0 by A3, Th4;
hence contradiction by A2, Th4; :: thesis: verum
end;
x - t <= y - t by A2, Th37;
hence x - t < y - t by A4, XXREAL_0:1; :: thesis: verum