let a, b, c, d be Real; :: thesis: ( a + b <= c - d implies a + d <= c - b )
assume a + b <= c - d ; :: thesis: a + d <= c - b
then (a + b) + d <= (c - d) + d by Lm5;
then ((a + b) + d) - b <= c - b by Th9;
hence a + d <= c - b ; :: thesis: verum