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