:: deftheorem Def2 defines -' XREAL_0:def 2 :
for r, s being Real holds
( ( r - s >= 0 implies r -' s = r - s ) & ( not r - s >= 0 implies r -' s = 0 ) );