let c, d, a, b be complex number ; :: thesis: ( c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c )
assume A1: ( c <> 0 & d <> 0 ) ; :: thesis: ( not a * c = b * d or a / d = b / c )
assume a * c = b * d ; :: thesis: a / d = b / c
then a = (b * d) / c by A1, Lm10;
then a = d * (b / c) by Lm9;
hence a / d = b / c by A1, Lm10; :: thesis: verum