let a, b, c, d be positive Real; :: thesis: ( ( ( a * b > c * d & a / b >= c / d ) or ( a * b >= c * d & a / b > c / d ) ) implies a > c )
A1: ( (a / b) * b = a & (c / d) * d = c ) by XCMPLX_1:87;
assume ( ( a * b > c * d & a / b >= c / d ) or ( a * b >= c * d & a / b > c / d ) ) ; :: thesis: a > c
then (a * b) * (a / b) > (c * d) * (c / d) by XREAL_1:98;
then a * a > c * c by A1;
hence a > c by XREAL_1:66; :: thesis: verum