let x, y, z be Element of REAL+ ; :: thesis: ( x <=' y implies x -' z <=' y -' z )
assume A1: x <=' y ; :: thesis: x -' z <=' y -' z
per cases ( z <=' x or not z <=' x ) ;
suppose A2: z <=' x ; :: thesis: x -' z <=' y -' z
then z <=' y by A1, Th3;
then A3: (y -' z) + z = y by Def1;
(x -' z) + z = x by A2, Def1;
hence x -' z <=' y -' z by A1, A3, Th7; :: thesis: verum
end;
suppose not z <=' x ; :: thesis: x -' z <=' y -' z
then x -' z = {} by Def1;
hence x -' z <=' y -' z by Th6; :: thesis: verum
end;
end;