theorem Th16: :: EUCLID_3:16
cpx2euc 0c = 0. (TOP-REAL 2) by COMPLEX1:4, EUCLID:54;