A1: sqrt 2 > 0 by SQUARE_1:25;
sqrt 2 < sqrt 4 by SQUARE_1:27;
then A2: (sqrt 2) / 2 < 2 / 2 by SQUARE_1:20, XREAL_1:74;
then ((sqrt 2) / 2) * (- 1) > 1 * (- 1) by XREAL_1:69;
then A3: - ((sqrt 2) / 2) in ].(- 1),1.[ by A1, XXREAL_1:4;
(sqrt 2) / 2 > 0 by A1, XREAL_1:139;
then (sqrt 2) / 2 in ].(- 1),1.[ by A2, XXREAL_1:4;
hence [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] c= ].(- 1),1.[ by A3, XXREAL_2:def 12; :: thesis: verum