theorem :: COMPLEX3:82
for a being positive light Real holds (1 / (1 + a)) + (1 / (1 - a)) > 2