let a, b be Real; :: thesis: ( 0 < a * b implies 0 < a / b )
assume A1: 0 < a * b ; :: thesis: 0 < a / b
then A2: b <> 0 ;
then 0 < b ^2 by SQUARE_1:12;
then 0 / (b ^2) < (a * b) / (b ^2) by A1;
then 0 < (a * b) / (b * b) by SQUARE_1:def 1;
then 0 < (a / b) * (b / b) by XCMPLX_1:76;
then 0 < (a / b) * 1 by A2, XCMPLX_1:60;
hence 0 < a / b ; :: thesis: verum