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