let x, y, s, t be R_eal; :: thesis: ( x <= y & s <= t implies x - t <= y - s )
assume A1: ( x <= y & s <= t ) ; :: thesis: x - t <= y - s
then - t <= - s by Lm3;
hence x - t <= y - s by A1, Th14; :: thesis: verum