sin | ].(PI / 2),((3 / 2) * PI ).[ c= sin | [.(PI / 2),((3 / 2) * PI ).] by RELAT_1:104, XXREAL_1:25;
then A1: rng (sin | ].(PI / 2),((3 / 2) * PI ).[) c= rng (sin | [.(PI / 2),((3 / 2) * PI ).]) by RELAT_1:25;
A2: rng (sin | ].(PI / 2),((3 / 2) * PI ).[) = sin .: ].(PI / 2),((3 / 2) * PI ).[ by RELAT_1:148;
thus sin .: ].(PI / 2),((3 / 2) * PI ).[ c= ].(- 1),1.[ :: according to XBOOLE_0:def 10 :: thesis: ].(- 1),1.[ c= sin .: ].(PI / 2),((3 / 2) * PI ).[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sin .: ].(PI / 2),((3 / 2) * PI ).[ or x in ].(- 1),1.[ )
assume A3: x in sin .: ].(PI / 2),((3 / 2) * PI ).[ ; :: thesis: x in ].(- 1),1.[
then consider a being set such that
A4: a in dom sin and
A5: a in ].(PI / 2),((3 / 2) * PI ).[ and
A6: sin . a = x by FUNCT_1:def 12;
reconsider a = a, x = x as Real by A4, A6;
set i = [\(a / (2 * PI ))/];
A7: H₁([\(a / (2 * PI ))/]) / ((2 * PI ) * 1) = [\(a / (2 * PI ))/] / 1 by XCMPLX_1:92;
A8: sin . a = sin a by SIN_COS:def 21;

A9: now

assume x = 1 ; :: thesis: contradiction
then A10: a = (PI / 2) + H₁([\(a / (2 * PI ))/]) by A6, A8, Th24;
then PI / 2 < (PI / 2) + H₁([\(a / (2 * PI ))/]) by A5, XXREAL_1:4;
then (PI / 2) - (PI / 2) < ((PI / 2) + H₁([\(a / (2 * PI ))/])) - (PI / 2) by XREAL_1:11;
then 0 < [\(a / (2 * PI ))/] ;
then A11: 0 + 1 <= [\(a / (2 * PI ))/] by INT_1:20;
(PI / 2) + H₁([\(a / (2 * PI ))/]) < (3 / 2) * PI by A5, A10, XXREAL_1:4;
then ((PI / 2) + H₁([\(a / (2 * PI ))/])) - (PI / 2) < ((3 / 2) * PI ) - (PI / 2) by XREAL_1:11;
then [\(a / (2 * PI ))/] < (1 * PI ) / (2 * PI ) by A7, XREAL_1:76;
then [\(a / (2 * PI ))/] < 1 / 2 by XCMPLX_1:92;
hence contradiction by A11, XXREAL_0:2; :: thesis: verum

end;

A12: now

assume x = - 1 ; :: thesis: contradiction
then A13: a = ((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/]) by A6, A8, Th23;
then ((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/]) < (3 / 2) * PI by A5, XXREAL_1:4;
then (((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/])) - ((3 / 2) * PI ) < ((3 / 2) * PI ) - ((3 / 2) * PI ) by XREAL_1:11;
then [\(a / (2 * PI ))/] < 0 ;
then A14: [\(a / (2 * PI ))/] <= - 1 by INT_1:21;
PI / 2 < ((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/]) by A5, A13, XXREAL_1:4;
then (PI / 2) - ((3 / 2) * PI ) < (((3 / 2) * PI ) + H₁([\(a / (2 * PI ))/])) - ((3 / 2) * PI ) by XREAL_1:11;
then ((- 1) * PI ) / (2 * PI ) < [\(a / (2 * PI ))/] by A7, XREAL_1:76;
then (- 1) / 2 < [\(a / (2 * PI ))/] by XCMPLX_1:92;
hence contradiction by A14, XXREAL_0:2; :: thesis: verum

end;

x <= 1 by A1, A2, A3, COMPTRIG:49, XXREAL_1:1;
then A15: x < 1 by A9, XXREAL_0:1;
- 1 <= x by A1, A2, A3, COMPTRIG:49, XXREAL_1:1;
then - 1 < x by A12, XXREAL_0:1;
hence x in ].(- 1),1.[ by A15, XXREAL_1:4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in ].(- 1),1.[ or a in sin .: ].(PI / 2),((3 / 2) * PI ).[ )
assume A16: a in ].(- 1),1.[ ; :: thesis: a in sin .: ].(PI / 2),((3 / 2) * PI ).[
then reconsider a = a as Real ;
( - 1 < a & a < 1 ) by A16, XXREAL_1:4;
then a in rng (sin | [.(PI / 2),((3 / 2) * PI ).]) by COMPTRIG:49, XXREAL_1:1;
then consider x being set such that
A17: x in dom (sin | [.(PI / 2),((3 / 2) * PI ).]) and
A18: (sin | [.(PI / 2),((3 / 2) * PI ).]) . x = a by FUNCT_1:def 5;
reconsider x = x as Real by A17;
A19: sin . x = a by A17, A18, FUNCT_1:70;
dom (sin | [.(PI / 2),((3 / 2) * PI ).]) = [.(PI / 2),((3 / 2) * PI ).] by RELAT_1:91, SIN_COS:27;
then ( PI / 2 <= x & x <= (3 / 2) * PI ) by A17, XXREAL_1:1;
then ( ( PI / 2 < x & x < (3 / 2) * PI ) or PI / 2 = x or (3 / 2) * PI = x ) by XXREAL_0:1;
then x in ].(PI / 2),((3 / 2) * PI ).[ by A16, A19, SIN_COS:81, XXREAL_1:4;
hence a in sin .: ].(PI / 2),((3 / 2) * PI ).[ by A19, FUNCT_1:def 12, SIN_COS:27; :: thesis: verum