let r be Real; :: thesis: ( 0 < r & r < 2 * PI implies cos r < 1 )
assume ( 0 < r & r < 2 * PI ) ; :: thesis: cos r < 1
then A1: cos r <> 1 by COMPTRIG:61;
cos r <= 1 by Th6;
hence cos r < 1 by A1, XXREAL_0:1; :: thesis: verum