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