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