let x, y be Element of REAL+ ; :: thesis: ( x - y = {} implies x = y )
A1: {} <> [{} ,(y -' x)] ;
assume A2: x - y = {} ; :: thesis: x = y
then A3: y <=' x by A1, ARYTM_1:def 2;
x -' y = {} by A1, A2, ARYTM_1:def 2;
hence x = y by A3, ARYTM_1:10; :: thesis: verum