thus tau_bar to_power 6 = tau_bar to_power (3 * 2)
.= (2 - (sqrt 5)) to_power 2 by Lm8, NEWTON:9
.= (2 - (sqrt 5)) ^2 by POWER:46
.= ((2 ^2) - ((2 * 2) * (sqrt 5))) + ((sqrt 5) ^2)
.= (4 - (4 * (sqrt 5))) + 5 by SQUARE_1:def 2
.= 9 - (4 * (sqrt 5)) ; :: thesis: verum