theorem :: ARYTM_1:19

for x, y being Element of REAL+ st x = {} & y <> {} holds
x - y = [{},y]