let r, s, t be Real; :: thesis: ( r >= 0 & s >= 0 & r + s < t implies ( r < t & s < t ) )
assume that
A1: ( r >= 0 & s >= 0 ) and
A2: r + s < t ; :: thesis: ( r < t & s < t )
assume ( r >= t or s >= t ) ; :: thesis: contradiction
then ( r + s >= t + 0 or s + r >= t + 0 ) by A1, XREAL_1:7;
hence contradiction by A2; :: thesis: verum