:: deftheorem Def1 defines heavy COMPLEX3:def 1 :
for a being Complex holds
( a is heavy iff |.a.| > 1 );