theorem :: COMPLEX3:11

for a being positive heavy Real
for b being non heavy Real holds
( a > b & b > - a )