let r, s be Real; :: thesis: ( 0 < r & 0 < s implies ( 0 <= r / (r + s) & r / (r + s) <= 1 ) )
assume that
A1: 0 < r and
A2: 0 < s ; :: thesis: ( 0 <= r / (r + s) & r / (r + s) <= 1 )
thus 0 <= r / (r + s) by A1, A2; :: thesis: r / (r + s) <= 1
0 + r <= s + r by A2, XREAL_1:6;
then r / (r + s) <= (r + s) / (r + s) by A1, XREAL_1:72;
hence r / (r + s) <= 1 by A1, A2, XCMPLX_1:60; :: thesis: verum