let x, y, z be Element of REAL+ ; :: thesis: ( x <=' y implies z -' y <=' z -' x )
assume A1: x <=' y ; :: thesis: z -' y <=' z -' x

per cases ( y <=' z or not y <=' z ) ;

suppose A2: y <=' z ; :: thesis: z -' y <=' z -' x

(z -' y) + x <=' (z -' y) + y by A1, Th7;
then A3: (z -' y) + x <=' z by A2, Def1;
x <=' z by A1, A2, Th3;
then (z -' y) + x <=' (z -' x) + x by A3, Def1;
hence z -' y <=' z -' x by Th7; :: thesis: verum

end;

suppose not y <=' z ; :: thesis: z -' y <=' z -' x

then z -' y = {} by Def1;
hence z -' y <=' z -' x by Th6; :: thesis: verum

end;

end;