let r be real number ; :: thesis: ( PI / 2 < r & r <= 2 * PI implies sin r < 1 )
assume that
A1: PI / 2 < r and
A2: r <= 2 * PI and
A3: sin r >= 1 ; :: thesis: contradiction
sin r <= 1 by Th4;
hence contradiction by A1, A2, A3, Th28, XXREAL_0:1; :: thesis: verum