:: deftheorem Def2 defines light COMPLEX3:def 2 :
for a being Complex holds
( a is light iff |.a.| < 1 );