let a, b be real number ; :: thesis: ( a in ].0 ,(PI / 2).[ & b in ].0 ,(PI / 2).[ implies ( a < b iff sin a < sin b ) )
assume A1: ( a in ].0 ,(PI / 2).[ & b in ].0 ,(PI / 2).[ ) ; :: 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 ].0 ,(PI / 2).[ /\ (dom sin ) & b in ].0 ,(PI / 2).[ /\ (dom sin ) ) by A1, XBOOLE_0:def 4, SIN_COS:27;
hence ( a < b implies sin a < sin b ) by A2, RFUNCT_2:43, SIN_COS2:2; :: 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:43, SIN_COS2:2; :: thesis: verum