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;