let x, y, t be ext-real number ; :: thesis: ( t <> -infty & t <> +infty & x < y implies x + t < y + t )
assume A1: ( t <> -infty & t <> +infty & x < y ) ; :: thesis: x + t < y + t
then A2: x + t <= y + t by Th36;
A3: t - t = 0 by Tx4;

now

assume x + t = y + t ; :: thesis: contradiction
then x + (t - t) = (y + t) - t by A1, Th60;
then x + 0 = y + (t - t) by A1, A3, Th60;
then x = y + 0 by A3, Tx3;
hence contradiction by A1, Tx3; :: thesis: verum

end;

hence x + t < y + t by A2, XXREAL_0:1; :: thesis: verum