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