theorem Th4: :: INT_4:4

for X being real-membered set
for a being Real holds
( ( a = 0 & not X is empty implies a ** X = {0} ) & ( not a ** X = {0} or a = 0 or X = {0} ) )