theorem :: COMPLEX3:37

for a, b being positive Real st a - b = a * b holds
b is light