:: deftheorem defines = COMPLEX1:def 3 :
for z1, z2 being Complex holds
( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) );