:: deftheorem Def2 defines - ARYTM_1:def 2 :
for x, y being Element of REAL+ holds
( ( y <=' x implies x - y = x -' y ) & ( not y <=' x implies x - y = [{},(y -' x)] ) );