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;