2
<
sqrt
5
by
SQUARE_1:20
,
SQUARE_1:27
;
then
not
0
+
(
sqrt
5
)
<=
1
by
XXREAL_0:2
;
then
0
*
2
>
(
1

(
sqrt
5
)
)
/
1
by
XREAL_1:19
;
then
(
1

(
sqrt
5
)
)
/
2
<
0
*
1
by
XREAL_1:113
;
hence
tau_bar
<
0
;
:: thesis:
verum