let a, b be complex number ; :: 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