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