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