sqrt 2 < sqrt 4 by SQUARE_1:95;
then A1: (sqrt 2) / 2 < 2 / 2 by SQUARE_1:85, XREAL_1:76;
then A2: ((sqrt 2) / 2) * (- 1) > 1 * (- 1) by XREAL_1:71;
sqrt 2 > 0 by SQUARE_1:93;
then A3: (sqrt 2) / 2 > 0 by XREAL_1:141;
then A4: (sqrt 2) / 2 in ].(- 1),1.[ by A1, XXREAL_1:4;
((sqrt 2) / 2) * (- 1) < 0 * (- 1) by A3, XREAL_1:71;
then - ((sqrt 2) / 2) in ].(- 1),1.[ by A2, XXREAL_1:4;
hence [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] c= ].(- 1),1.[ by A4, XXREAL_2:def 12; :: thesis: verum