let b, c, d be Real; :: thesis: ( b > 0 & c > 0 & d > 0 implies (b - d) / (b / c) < c )
assume A1: ( b > 0 & c > 0 & d > 0 ) ; :: thesis: (b - d) / (b / c) < c
then (- d) + b < 0 + b by XREAL_1:8;
then (b - d) / b < b / b by A1, XREAL_1:74;
then (b - d) / b < 1 by A1, XCMPLX_1:60;
then ((b - d) / b) * c < 1 * c by A1, XREAL_1:68;
hence (b - d) / (b / c) < c by XCMPLX_1:82; :: thesis: verum