consider ix being Integer, nx being Nat such that
A1: x = ix / (2 |^ nx) by Th18;
- x = (- ix) / (2 |^ nx) by A1, XCMPLX_1:187;
hence - x is dyadic-like ; :: thesis: verum