let x, y, t be R_eal; :: 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 SUPINF_2:15;
A3: t - t = 0 by EXTREAL1:9;

now

assume x - t = y - t ; :: thesis: contradiction
then x - (t - t) = (y - t) + t by A1, EXTREAL2:41;
then x - (R_EAL 0 ) = y - (t - t) by A1, A3, EXTREAL2:41;
then x = y + (R_EAL 0 ) by A3, EXTREAL1:24, SUPINF_2:18;
hence contradiction by A1, SUPINF_2:18; :: thesis: verum

end;

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