let a, b be Complex; :: thesis: 1 / (a / b) = b / a
thus 1 / (a / b) = 1 / (a * (b ")) by XCMPLX_0:def 9
.= (a * (b ")) " by Lm4
.= b * (a ") by Lm11
.= b / a by XCMPLX_0:def 9 ; :: thesis: verum