let r be Real; :: thesis: ( 0 <= r & r < PI implies cos r > - 1 )
assume that
A1: 0 <= r and
A2: r < PI ; :: thesis: cos r > - 1
A3: cos r >= - 1 by Th5;
r <= 2 * PI by A2, Lm10, XXREAL_0:2;
hence cos r > - 1 by A1, A2, A3, Th29, XXREAL_0:1; :: thesis: verum