let a, b, c, d be Real; :: thesis: ( a - b <= c + d implies a - d <= c + b )
assume c + d >= a - b ; :: thesis: a - d <= c + b

per cases then ( c + d >= a - b or d + c >= a - b ) ;

suppose c + d >= a - b ; :: thesis: a - d <= c + b

then (c + d) + b >= a by Lm19;
then (c + b) + d >= a ;
hence a - d <= c + b by Lm18; :: thesis: verum

end;

suppose d + c >= a - b ; :: thesis: a - d <= c + b

then (c + d) + b >= a by Lm19;
then (c + b) + d >= a ;
hence a - d <= c + b by Lm18; :: thesis: verum

end;

end;