let x, y, z be Element of REAL+ ; :: thesis: ( y <=' x implies ( z + y <=' x iff z <=' x -' y ) )
assume y <=' x ; :: thesis: ( z + y <=' x iff z <=' x -' y )
then (x -' y) + y = x by Def1;
hence ( z + y <=' x iff z <=' x -' y ) by Th7; :: thesis: verum