let a, b, c, d be Real; :: thesis: ( (a / b) - c <> 0 & d <> 0 & b <> 0 & a = (b * c) + d implies 1 / ((a / b) - c) = b / d )
assume that
A1: ( (a / b) - c <> 0 & d <> 0 ) and
A2: b <> 0 ; :: thesis: ( not a = (b * c) + d or 1 / ((a / b) - c) = b / d )
assume a = (b * c) + d ; :: thesis: 1 / ((a / b) - c) = b / d
then d = b * ((a - (b * c)) / b) by A2, XCMPLX_1:87
.= b * ((a / b) - ((b * c) / b)) ;
then 1 * d = b * ((a / b) - c) by A2, XCMPLX_1:89;
hence 1 / ((a / b) - c) = b / d by A1, XCMPLX_1:94; :: thesis: verum