let x, y, z, w be ExtReal; :: thesis: ( x <= y & z <= w implies x - w <= y - z )
assume that
A1: x <= y and
A2: z <= w ; :: thesis: x - w <= y - z
- w <= - z by A2, Lm15;
hence x - w <= y - z by A1, Th36; :: thesis: verum