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