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