theorem :: ARYTM_1:2

for x, y being Element of REAL+ holds
( not x *' y = {} or x = {} or y = {} )