theorem :: BKMODEL4:2

for a, b being Real st 0 < a * b holds
0 < a / b