theorem :: XREAL_1:139

for a, b being Real st 0 < a & 0 < b holds
0 < a / b ;