let x, y be Element of REAL+ ; :: thesis: x -' y <=' x

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

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

then (x -' y) + y = x by Def1;
hence x -' y <=' x by ARYTM_2:19; :: thesis: verum

end;

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

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

end;

end;