2
<
sqrt
5
by
SQUARE_1:20
,
SQUARE_1:27
;
then
1
<
sqrt
5
by
XXREAL_0:2
;
then
1
+
1
<
1
+
(
sqrt
5
)
by
XREAL_1:8
;
then
2
/
2
<
(
1
+
(
sqrt
5
)
)
/
2
by
XREAL_1:74
;
hence
1
<
tau
;
:: thesis:
verum