:: deftheorem defines cpx2euc EUCLID_3:def 1 :
for z being Complex holds cpx2euc z = |[(Re z),(Im z)]|;