for x being Real st x <> 0 holds
for A being Subset of REAL st A = REAL holds
x ** A = A