let a, b be Real; :: thesis: ( a in ].(PI / 2),PI.[ & b in ].(PI / 2),PI.[ implies ( a < b iff sin a > sin b ) )
assume ( a in ].(PI / 2),PI.[ & b in ].(PI / 2),PI.[ ) ; :: thesis: ( a < b iff sin a > sin b )
then A1: ( a in ].(PI / 2),PI.[ /\ (dom sin) & b in ].(PI / 2),PI.[ /\ (dom sin) ) by SIN_COS:24, XBOOLE_0:def 4;
A2: ( sin a = sin . a & sin b = sin . b ) by SIN_COS:def 17;
hence ( a < b implies sin a > sin b ) by A1, RFUNCT_2:21, SIN_COS2:3; :: thesis: ( sin a > sin b implies a < b )
assume A3: sin a > sin b ; :: thesis: a < b
assume a >= b ; :: thesis: contradiction
then a > b by A3, XXREAL_0:1;
hence contradiction by A2, A1, A3, RFUNCT_2:21, SIN_COS2:3; :: thesis: verum