:: deftheorem Def1 defines -' ARYTM_1:def 1 :
for x, y, b₃ being Element of REAL+ holds
( ( y <=' x implies ( b₃ = x -' y iff b₃ + y = x ) ) & ( not y <=' x implies ( b₃ = x -' y iff b₃ = {} ) ) );