let x, y be Real; :: thesis: |.((sin x) - (sin y)).| <= |.(x - y).|
A2: |.((sin x) - (sin y)).| = |.(2 * ((cos ((x + y) / 2)) * (sin ((x - y) / 2)))).| by SIN_COS4:16
.= |.2.| * |.((cos ((x + y) / 2)) * (sin ((x - y) / 2))).| by COMPLEX1:65
.= |.2.| * (|.(cos ((x + y) / 2)).| * |.(sin ((x - y) / 2)).|) by COMPLEX1:65
.= (|.2.| * |.(cos ((x + y) / 2)).|) * |.(sin ((x - y) / 2)).|
.= (2 * |.(cos ((x + y) / 2)).|) * |.(sin ((x - y) / 2)).| by COMPLEX1:43 ;
( 0 <= |.(cos ((x + y) / 2)).| & |.(cos ((x + y) / 2)).| <= 1 & 0 <= |.((x - y) / 2).| & |.(sin ((x - y) / 2)).| <= |.((x - y) / 2).| ) by SIN_COS:27, LmSin1, COMPLEX1:46;
then ( |.(sin ((x - y) / 2)).| * |.(cos ((x + y) / 2)).| <= |.((x - y) / 2).| * |.(cos ((x + y) / 2)).| & |.(cos ((x + y) / 2)).| * |.((x - y) / 2).| <= 1 * |.((x - y) / 2).| ) by XREAL_1:64;
then |.(cos ((x + y) / 2)).| * |.(sin ((x - y) / 2)).| <= 1 * |.((x - y) / 2).| by XXREAL_0:2;
then AA: (|.(cos ((x + y) / 2)).| * |.(sin ((x - y) / 2)).|) * 2 <= (1 * |.((x - y) / 2).|) * 2 by XREAL_1:64;
(1 * |.((x - y) / 2).|) * 2 = (|.(x - y).| / |.2.|) * 2 by COMPLEX1:67
.= (|.(x - y).| / 2) * 2 by COMPLEX1:43
.= |.(x - y).| ;
hence |.((sin x) - (sin y)).| <= |.(x - y).| by AA, A2; :: thesis: verum