theorem :: COMPLEX1:76

for a being Real holds
( - |.a.| <= a & a <= |.a.| ) by Lm29;