euc2cpx (0. (TOP-REAL 2)) = 0c by Th1, Th16;