let t, p, s be Real; :: thesis: ( 0 < s & t <= p implies ( t < p + s & t - s < p ) )
assume ( 0 < s & t <= p ) ; :: thesis: ( t < p + s & t - s < p )
then t + 0 < p + s by XREAL_1:8;
hence ( t < p + s & t - s < p ) by XREAL_1:19; :: thesis: verum