theorem :: XCMPLX_1:213

for a, b being Complex holds (a / b) " = b / a by Lm7;