A1: delta (1,(- 1),(- 1)) = ((- 1) ^2) - ((4 * 1) * (- 1)) by QUIN_1:def 1
.= 5 ;
then A2: ((- (- 1)) - (sqrt (delta (1,(- 1),(- 1))))) / (2 * 1) = tau_bar ;
A3: for x being Real st ( x = tau or x = tau_bar ) holds
x ^2 = x + 1

proof

let x be Real; :: thesis: ( ( x = tau or x = tau_bar ) implies x ^2 = x + 1 )
assume ( x = tau or x = tau_bar ) ; :: thesis: x ^2 = x + 1
then ((1 * (x ^2)) + ((- 1) * x)) + (- 1) = 0 by A1, A2, Th6;
hence x ^2 = x + 1 ; :: thesis: verum

end;

hence tau ^2 = tau + 1 ; :: thesis: tau_bar ^2 = tau_bar + 1
thus tau_bar ^2 = tau_bar + 1 by A3; :: thesis: verum