:: deftheorem Def3 defines weightless COMPLEX3:def 3 :
for a being Complex holds
( a is weightless iff ( |.a.| = 0 or |.a.| = 1 ) );