let r be real number ; :: 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, Lm13, XXREAL_0:2;
then cos r <> - 1 by A1, A2, Th29;
hence cos r > - 1 by A3, XXREAL_0:1; :: thesis: verum