let a, b be Real; :: thesis: ( a in ].0,(PI / 2).[ & b in ].0,(PI / 2).[ implies ( a < b iff sin a < sin b ) )
assume ( a in ].0,(PI / 2).[ & b in ].0,(PI / 2).[ ) ; :: thesis: ( a < b iff sin a < sin b )
then A1: ( a in ].0,(PI / 2).[ /\ (dom sin) & b in ].0,(PI / 2).[ /\ (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:20, SIN_COS2:2; :: 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:20, SIN_COS2:2; :: thesis: verum