let x, r be Real; :: thesis: ( 0 <= x & x <= 1 & r > - 1 implies (x * r) + 1 > 0 )
assume AA: ( 0 <= x & x <= 1 & r > - 1 ) ; :: thesis: (x * r) + 1 > 0

per cases ( r < 0 or r >= 0 ) ;

suppose r < 0 ; :: thesis: (x * r) + 1 > 0

then r <= r * x by XREAL_1:152, AA;
then - 1 < r * x by XXREAL_0:2, AA;
then (x * r) + 1 > (- 1) + 1 by XREAL_1:8;
hence (x * r) + 1 > 0 ; :: thesis: verum

end;

suppose r >= 0 ; :: thesis: (x * r) + 1 > 0

hence (x * r) + 1 > 0 by AA; :: thesis: verum

end;

end;