let x be Element of REAL+ ; :: thesis: x - x = {}
x <=' x ;
then x - x = x -' x by Def2;
hence x - x = {} by Lm3; :: thesis: verum