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