theorem :: COMPLEX1:70

for a being Real st a <= 0 holds
|.a.| = - a by Lm27;