let x, y be Element of REAL+ ; :: thesis: ( x <=' y or x -' y <> {} )
assume A1: not x <=' y ; :: thesis: x -' y <> {}
then A2: (x -' y) + y = x by Def1;
assume x -' y = {} ; :: thesis: contradiction
then x = y by A2, ARYTM_2:def 8;
hence contradiction by A1; :: thesis: verum