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