:: deftheorem Def3 defines imaginary BASEL_2:def 3 :
for z being Complex holds
( z is imaginary iff Re z = 0 );