theorem Th17: :: EUCLID_3:17

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