let x be Element of REAL+ ; :: thesis: x -' x = {}
x <=' x ;
then (x -' x) + x = x by Def1;
hence x -' x = {} by Th1; :: thesis: verum