theorem THJD: :: GTARSKI2:4

for r, s being Real st 0 < r & 0 < s holds
( 0 <= r / (r + s) & r / (r + s) <= 1 )