let x, y, z, w be ext-real number ; :: thesis: ( x <= y & z <= w implies x - w <= y - z )
assume A1: ( x <= y & z <= w ) ; :: thesis: x - w <= y - z
then - w <= - z by Lm3;
hence x - w <= y - z by A1, Th36; :: thesis: verum